Theorem inf3lem2 3465

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 3471 for detailed description.

Hypotheses

Ref	Expression
inf3lem.1	|- G = {<.y, z>. | z = {w e. x | (w i^i x) (_ y}}
inf3lem.2	|- F = (rec(G, (/)) |` om)
inf3lem.3	|- A e. V
inf3lem.4	|- B e. V

Assertion

Ref	Expression
inf3lem2	|- ((-. x = (/) /\ x (_ U.x) -> (A e. om -> -. (F` A) = x))

Distinct variable group(s):   x,y,z,w

Proof of Theorem inf3lem2

Step	Hyp	Ref	Expression
1		fveq2 2832	. . . . . 6 |- (v = (/) -> (F` v) = (F` (/)))
2	1	cleq1d 1109	. . . . 5 |- (v = (/) -> ((F` v) = x <-> (F` (/)) = x))
3	2	negbid 463	. . . 4 |- (v = (/) -> (-. (F` v) = x <-> -. (F` (/)) = x))
4	3	imbi2d 464	. . 3 |- (v = (/) -> (((-. x = (/) /\ x (_ U.x) -> -. (F` v) = x) <-> ((-. x = (/) /\ x (_ U.x) -> -. (F` (/)) = x)))
5		fveq2 2832	. . . . . 6 |- (v = u -> (F` v) = (F` u))
6	5	cleq1d 1109	. . . . 5 |- (v = u -> ((F` v) = x <-> (F` u) = x))
7	6	negbid 463	. . . 4 |- (v = u -> (-. (F` v) = x <-> -. (F` u) = x))
8	7	imbi2d 464	. . 3 |- (v = u -> (((-. x = (/) /\ x (_ U.x) -> -. (F` v) = x) <-> ((-. x = (/) /\ x (_ U.x) -> -. (F` u) = x)))
9		fveq2 2832	. . . . . 6 |- (v = suc u -> (F` v) = (F` suc u))
10	9	cleq1d 1109	. . . . 5 |- (v = suc u -> ((F` v) = x <-> (F` suc u) = x))
11	10	negbid 463	. . . 4 |- (v = suc u -> (-. (F` v) = x <-> -. (F` suc u) = x))
12	11	imbi2d 464	. . 3 |- (v = suc u -> (((-. x = (/) /\ x (_ U.x) -> -. (F` v) = x) <-> ((-. x = (/) /\ x (_ U.x) -> -. (F` suc u) = x)))
13		fveq2 2832	. . . . . 6 |- (v = A -> (F` v) = (F` A))
14	13	cleq1d 1109	. . . . 5 |- (v = A -> ((F` v) = x <-> (F` A) = x))
15	14	negbid 463	. . . 4 |- (v = A -> (-. (F` v) = x <-> -. (F` A) = x))
16	15	imbi2d 464	. . 3 |- (v = A -> (((-. x = (/) /\ x (_ U.x) -> -. (F` v) = x) <-> ((-. x = (/) /\ x (_ U.x) -> -. (F` A) = x)))
17		inf3lem.1	. . . . . . . . 9 |- G = {<.y, z>. | z = {w e. x | (w i^i x) (_ y}}
18		inf3lem.2	. . . . . . . . 9 |- F = (rec(G, (/)) |` om)
19		inf3lem.3	. . . . . . . . 9 |- A e. V
20		inf3lem.4	. . . . . . . . 9 |- B e. V
21	17, 18, 19, 20	inf3lemb 3461	. . . . . . . 8 |- (F` (/)) = (/)
22	21	cleq1i 1108	. . . . . . 7 |- ((F` (/)) = x <-> (/) = x)
23		cleqcom 1103	. . . . . . 7 |- ((/) = x <-> x = (/))
24	22, 23	bitr 151	. . . . . 6 |- ((F` (/)) = x <-> x = (/))
25	24	biimp 133	. . . . 5 |- ((F` (/)) = x -> x = (/))
26	25	con3i 90	. . . 4 |- (-. x = (/) -> -. (F` (/)) = x)
27	26	adantr 306	. . 3 |- ((-. x = (/) /\ x (_ U.x) -> -. (F` (/)) = x)
28		ssel 1502	. . . . . . . . . . . . . . 15 |- (x (_ U.x -> (v e. x -> v e. U.x))
29		eluni 1922	. . . . . . . . . . . . . . 15 |- (v e. U.x <-> E.f(v e. f /\ f e. x))
30	28, 29	syl6ib 185	. . . . . . . . . . . . . 14 |- (x (_ U.x -> (v e. x -> E.f(v e. f /\ f e. x)))
31		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . 24 |- u e. V
32	17, 18, 31, 20	inf3lemc 3462	. . . . . . . . . . . . . . . . . . . . . . 23 |- (u e. om -> (F` suc u) = (G` (F` u)))
33	32	eleq2d 1156	. . . . . . . . . . . . . . . . . . . . . 22 |- (u e. om -> (f e. (F` suc u) <-> f e. (G` (F` u))))
34		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- f e. V
35		fvex 2838	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (F` u) e. V
36	17, 18, 34, 35	inf3lema 3460	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f e. (G` (F` u)) <-> (f e. x /\ (f i^i x) (_ (F` u)))
37	36	pm3.27bd 263	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f e. (G` (F` u)) -> (f i^i x) (_ (F` u))
38	37	sseld 1506	. . . . . . . . . . . . . . . . . . . . . . 23 |- (f e. (G` (F` u)) -> (v e. (f i^i x) -> v e. (F` u)))
39		elin 1635	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v e. (f i^i x) <-> (v e. f /\ v e. x))
40	38, 39	syl5ibr 182	. . . . . . . . . . . . . . . . . . . . . 22 |- (f e. (G` (F` u)) -> ((v e. f /\ v e. x) -> v e. (F` u)))
41	33, 40	syl6bi 187	. . . . . . . . . . . . . . . . . . . . 21 |- (u e. om -> (f e. (F` suc u) -> ((v e. f /\ v e. x) -> v e. (F` u))))
42		eleq2 1150	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F` suc u) = x -> (f e. (F` suc u) <-> f e. x))
43	42	biimparc 327	. . . . . . . . . . . . . . . . . . . . 21 |- ((f e. x /\ (F` suc u) = x) -> f e. (F` suc u))
44	41, 43	syl5 22	. . . . . . . . . . . . . . . . . . . 20 |- (u e. om -> ((f e. x /\ (F` suc u) = x) -> ((v e. f /\ v e. x) -> v e. (F` u))))
45	44	com23 32	. . . . . . . . . . . . . . . . . . 19 |- (u e. om -> ((v e. f /\ v e. x) -> ((f e. x /\ (F` suc u) = x) -> v e. (F` u))))
46	45	exp4a 295	. . . . . . . . . . . . . . . . . 18 |- (u e. om -> ((v e. f /\ v e. x) -> (f e. x -> ((F` suc u) = x -> v e. (F` u)))))
47	46	exp3a 292	. . . . . . . . . . . . . . . . 17 |- (u e. om -> (v e. f -> (v e. x -> (f e. x -> ((F` suc u) = x -> v e. (F` u))))))
48	47	com34 36	. . . . . . . . . . . . . . . 16 |- (u e. om -> (v e. f -> (f e. x -> (v e. x -> ((F` suc u) = x -> v e. (F` u))))))
49	48	imp3a 279	. . . . . . . . . . . . . . 15 |- (u e. om -> ((v e. f /\ f e. x) -> (v e. x -> ((F` suc u) = x -> v e. (F` u)))))
50	49	19.23adv 954	. . . . . . . . . . . . . 14 |- (u e. om -> (E.f(v e. f /\ f e. x) -> (v e. x -> ((F` suc u) = x -> v e. (F` u)))))
51	30, 50	sylan9r 360	. . . . . . . . . . . . 13 |- ((u e. om /\ x (_ U.x) -> (v e. x -> (v e. x -> ((F` suc u) = x -> v e. (F` u)))))
52	51	pm2.43d 59	. . . . . . . . . . . 12 |- ((u e. om /\ x (_ U.x) -> (v e. x -> ((F` suc u) = x -> v e. (F` u))))
53		con3 86	. . . . . . . . . . . 12 |- (((F` suc u) = x -> v e. (F` u)) -> (-. v e. (F` u) -> -. (F` suc u) = x))
54	52, 53	syl6 23	. . . . . . . . . . 11 |- ((u e. om /\ x (_ U.x) -> (v e. x -> (-. v e. (F` u) -> -. (F` suc u) = x)))
55	54	imp3a 279	. . . . . . . . . 10 |- ((u e. om /\ x (_ U.x) -> ((v e. x /\ -. v e. (F` u)) -> -. (F` suc u) = x))
56	55	19.23adv 954	. . . . . . . . 9 |- ((u e. om /\ x (_ U.x) -> (E.v(v e. x /\ -. v e. (F` u)) -> -. (F` suc u) = x))
57		dfpss2 1557	. . . . . . . . . 10 |- ((F` u) (. x <-> ((F` u) (_ x /\ -. (F` u) = x))
58		pssnel 1752	. . . . . . . . . 10 |- ((F` u) (. x -> E.v(v e. x /\ -. v e. (F` u)))
59	57, 58	sylbir 176	. . . . . . . . 9 |- (((F` u) (_ x /\ -. (F` u) = x) -> E.v(v e. x /\ -. v e. (F` u)))
60	56, 59	syl5 22	. . . . . . . 8 |- ((u e. om /\ x (_ U.x) -> (((F` u) (_ x /\ -. (F` u) = x) -> -. (F` suc u) = x))
61	17, 18, 31, 20	inf3lemd 3463	. . . . . . . 8 |- (u e. om -> (F` u) (_ x)
62	60, 61	sylani 356	. . . . . . 7 |- ((u e. om /\ x (_ U.x) -> ((u e. om /\ -. (F` u) = x) -> -. (F` suc u) = x))
63	62	exp4b 296	. . . . . 6 |- (u e. om -> (x (_ U.x -> (u e. om -> (-. (F` u) = x -> -. (F` suc u) = x))))
64	63	pm2.43a 60	. . . . 5 |- (u e. om -> (x (_ U.x -> (-. (F` u) = x -> -. (F` suc u) = x)))
65	64	adantld 307	. . . 4 |- (u e. om -> ((-. x = (/) /\ x (_ U.x) -> (-. (F` u) = x -> -. (F` suc u) = x)))
66	65	a2d 15	. . 3 |- (u e. om -> (((-. x = (/) /\ x (_ U.x) -> -. (F` u) = x) -> ((-. x = (/) /\ x (_ U.x) -> -. (F` suc u) = x)))
67	4, 8, 12, 16, 27, 66	finds 2397	. 2 |- (A e. om -> ((-. x = (/) /\ x (_ U.x) -> -. (F` A) = x))
68	67	com12 13	1 |-