Theorem inf3lem2 4614

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4620 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:   x,y,z,w

Proof of Theorem inf3lem2

Step	Hyp	Ref	Expression
1		fveq2 3724	. . . . 5 |- (v = (/) -> (F` v) = (F` (/)))
2	1	neeq1d 1594	. . . 4 |- (v = (/) -> ((F` v) =/= x <-> (F` (/)) =/= x))
3	2	imbi2d 612	. . 3 |- (v = (/) -> (((x =/= (/) /\ x (_ U.x) -> (F` v) =/= x) <-> ((x =/= (/) /\ x (_ U.x) -> (F` (/)) =/= x)))
4		fveq2 3724	. . . . 5 |- (v = u -> (F` v) = (F` u))
5	4	neeq1d 1594	. . . 4 |- (v = u -> ((F` v) =/= x <-> (F` u) =/= x))
6	5	imbi2d 612	. . 3 |- (v = u -> (((x =/= (/) /\ x (_ U.x) -> (F` v) =/= x) <-> ((x =/= (/) /\ x (_ U.x) -> (F` u) =/= x)))
7		fveq2 3724	. . . . 5 |- (v = suc u -> (F` v) = (F` suc u))
8	7	neeq1d 1594	. . . 4 |- (v = suc u -> ((F` v) =/= x <-> (F` suc u) =/= x))
9	8	imbi2d 612	. . 3 |- (v = suc u -> (((x =/= (/) /\ x (_ U.x) -> (F` v) =/= x) <-> ((x =/= (/) /\ x (_ U.x) -> (F` suc u) =/= x)))
10		fveq2 3724	. . . . 5 |- (v = A -> (F` v) = (F` A))
11	10	neeq1d 1594	. . . 4 |- (v = A -> ((F` v) =/= x <-> (F` A) =/= x))
12	11	imbi2d 612	. . 3 |- (v = A -> (((x =/= (/) /\ x (_ U.x) -> (F` v) =/= x) <-> ((x =/= (/) /\ x (_ U.x) -> (F` A) =/= x)))
13		inf3lem.1	. . . . . . . . 9 |- G = {<.y, z>. | z = {w e. x | (w i^i x) (_ y}}
14		inf3lem.2	. . . . . . . . 9 |- F = (rec(G, (/)) |` om)
15		inf3lem.3	. . . . . . . . 9 |- A e. V
16		inf3lem.4	. . . . . . . . 9 |- B e. V
17	13, 14, 15, 16	inf3lemb 4610	. . . . . . . 8 |- (F` (/)) = (/)
18	17	eqeq1i 1482	. . . . . . 7 |- ((F` (/)) = x <-> (/) = x)
19		eqcom 1477	. . . . . . 7 |- ((/) = x <-> x = (/))
20	18, 19	bitr 173	. . . . . 6 |- ((F` (/)) = x <-> x = (/))
21	20	biimp 151	. . . . 5 |- ((F` (/)) = x -> x = (/))
22	21	necon3i 1605	. . . 4 |- (x =/= (/) -> (F` (/)) =/= x)
23	22	adantr 389	. . 3 |- ((x =/= (/) /\ x (_ U.x) -> (F` (/)) =/= x)
24		ssel 2063	. . . . . . . . . . . . . . 15 |- (x (_ U.x -> (v e. x -> v e. U.x))
25		eluni 2506	. . . . . . . . . . . . . . 15 |- (v e. U.x <-> E.f(v e. f /\ f e. x))
26	24, 25	syl6ib 212	. . . . . . . . . . . . . 14 |- (x (_ U.x -> (v e. x -> E.f(v e. f /\ f e. x)))
27		visset 1813	. . . . . . . . . . . . . . . . . . . . . . . 24 |- u e. V
28	13, 14, 27, 16	inf3lemc 4611	. . . . . . . . . . . . . . . . . . . . . . 23 |- (u e. om -> (F` suc u) = (G` (F` u)))
29	28	eleq2d 1541	. . . . . . . . . . . . . . . . . . . . . 22 |- (u e. om -> (f e. (F` suc u) <-> f e. (G` (F` u))))
30		visset 1813	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- f e. V
31		fvex 3732	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (F` u) e. V
32	13, 14, 30, 31	inf3lema 4609	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f e. (G` (F` u)) <-> (f e. x /\ (f i^i x) (_ (F` u)))
33	32	pm3.27bi 326	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f e. (G` (F` u)) -> (f i^i x) (_ (F` u))
34	33	sseld 2067	. . . . . . . . . . . . . . . . . . . . . . 23 |- (f e. (G` (F` u)) -> (v e. (f i^i x) -> v e. (F` u)))
35		elin 2207	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v e. (f i^i x) <-> (v e. f /\ v e. x))
36	34, 35	syl5ibr 207	. . . . . . . . . . . . . . . . . . . . . 22 |- (f e. (G` (F` u)) -> ((v e. f /\ v e. x) -> v e. (F` u)))
37	29, 36	syl6bi 214	. . . . . . . . . . . . . . . . . . . . 21 |- (u e. om -> (f e. (F` suc u) -> ((v e. f /\ v e. x) -> v e. (F` u))))
38		eleq2 1535	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F` suc u) = x -> (f e. (F` suc u) <-> f e. x))
39	38	biimparc 419	. . . . . . . . . . . . . . . . . . . . 21 |- ((f e. x /\ (F` suc u) = x) -> f e. (F` suc u))
40	37, 39	syl5 21	. . . . . . . . . . . . . . . . . . . 20 |- (u e. om -> ((f e. x /\ (F` suc u) = x) -> ((v e. f /\ v e. x) -> v e. (F` u))))
41	40	com23 32	. . . . . . . . . . . . . . . . . . 19 |- (u e. om -> ((v e. f /\ v e. x) -> ((f e. x /\ (F` suc u) = x) -> v e. (F` u))))
42	41	exp4a 378	. . . . . . . . . . . . . . . . . 18 |- (u e. om -> ((v e. f /\ v e. x) -> (f e. x -> ((F` suc u) = x -> v e. (F` u)))))
43	42	exp3a 375	. . . . . . . . . . . . . . . . 17 |- (u e. om -> (v e. f -> (v e. x -> (f e. x -> ((F` suc u) = x -> v e. (F` u))))))
44	43	com34 36	. . . . . . . . . . . . . . . 16 |- (u e. om -> (v e. f -> (f e. x -> (v e. x -> ((F` suc u) = x -> v e. (F` u))))))
45	44	imp3a 361	. . . . . . . . . . . . . . 15 |- (u e. om -> ((v e. f /\ f e. x) -> (v e. x -> ((F` suc u) = x -> v e. (F` u)))))
46	45	19.23adv 1214	. . . . . . . . . . . . . 14 |- (u e. om -> (E.f(v e. f /\ f e. x) -> (v e. x -> ((F` suc u) = x -> v e. (F` u)))))
47	26, 46	sylan9r 469	. . . . . . . . . . . . 13 |- ((u e. om /\ x (_ U.x) -> (v e. x -> (v e. x -> ((F` suc u) = x -> v e. (F` u)))))
48	47	pm2.43d 65	. . . . . . . . . . . 12 |- ((u e. om /\ x (_ U.x) -> (v e. x -> ((F` suc u) = x -> v e. (F` u))))
49		id 59	. . . . . . . . . . . . 13 |- (((F` suc u) = x -> v e. (F` u)) -> ((F` suc u) = x -> v e. (F` u)))
50	49	necon3bd 1603	. . . . . . . . . . . 12 |- (((F` suc u) = x -> v e. (F` u)) -> (-. v e. (F` u) -> (F` suc u) =/= x))
51	48, 50	syl6 22	. . . . . . . . . . 11 |- ((u e. om /\ x (_ U.x) -> (v e. x -> (-. v e. (F` u) -> (F` suc u) =/= x)))
52	51	imp3a 361	. . . . . . . . . 10 |- ((u e. om /\ x (_ U.x) -> ((v e. x /\ -. v e. (F` u)) -> (F` suc u) =/= x))
53	52	19.23adv 1214	. . . . . . . . 9 |- ((u e. om /\ x (_ U.x) -> (E.v(v e. x /\ -. v e. (F` u)) -> (F` suc u) =/= x))
54		df-pss 2055	. . . . . . . . . 10 |- ((F` u) (. x <-> ((F` u) (_ x /\ (F` u) =/= x))
55		pssnel 2331	. . . . . . . . . 10 |- ((F` u) (. x -> E.v(v e. x /\ -. v e. (F` u)))
56	54, 55	sylbir 201	. . . . . . . . 9 |- (((F` u) (_ x /\ (F` u) =/= x) -> E.v(v e. x /\ -. v e. (F` u)))
57	53, 56	syl5 21	. . . . . . . 8 |- ((u e. om /\ x (_ U.x) -> (((F` u) (_ x /\ (F` u) =/= x) -> (F` suc u) =/= x))
58	13, 14, 27, 16	inf3lemd 4612	. . . . . . . 8 |- (u e. om -> (F` u) (_ x)
59	57, 58	sylani 464	. . . . . . 7 |- ((u e. om /\ x (_ U.x) -> ((u e. om /\ (F` u) =/= x) -> (F` suc u) =/= x))
60	59	exp4b 379	. . . . . 6 |- (u e. om -> (x (_ U.x -> (u e. om -> ((F` u) =/= x -> (F` suc u) =/= x))))
61	60	pm2.43a 66	. . . . 5 |- (u e. om -> (x (_ U.x -> ((F` u) =/= x -> (F` suc u) =/= x)))
62	61	adantld 390	. . . 4 |- (u e. om -> ((x =/= (/) /\ x (_ U.x) -> ((F` u) =/= x -> (F` suc u) =/= x)))
63	62	a2d 13	. . 3 |- (u e. om -> (((x =/= (/) /\ x (_ U.x) -> (F` u) =/= x) -> ((x =/= (/) /\ x (_ U.x) -> (F` suc u) =/= x)))
64	3, 6, 9, 12, 23, 63	finds 3156	. 2 |- (A e. om -> ((x =/= (/) /\ x (_ U.x) -> (F` A) =/= x))
65	64	com12 11	1 |- ((x =/= (/) /\ x (_ U.x) -> (A e. om -> (F` A) =/= x))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 223   = wceq 956   e. wcel 958  E.wex 980   =/= wne 1585  {crab 1648