Theorem onfr 2983

Description: The ordinal class is founded. This lemma is needed for ordon 2984 in order to eliminate the need for the Axiom of Regularity.

Assertion

Ref	Expression
onfr	|- E Fr On

Proof of Theorem onfr

Step	Hyp	Ref	Expression
1		dfepfr 2929	. 2 |- (E Fr On <-> A.x((x (_ On /\ x =/= (/)) -> E.z e. x (x i^i z) = (/)))
2		ineq2 2209	. . . . . . . . . 10 |- (z = y -> (x i^i z) = (x i^i y))
3	2	eqeq1d 1482	. . . . . . . . 9 |- (z = y -> ((x i^i z) = (/) <-> (x i^i y) = (/)))
4	3	rcla4ev 1875	. . . . . . . 8 |- ((y e. x /\ (x i^i y) = (/)) -> E.z e. x (x i^i z) = (/))
5	4	expcom 374	. . . . . . 7 |- ((x i^i y) = (/) -> (y e. x -> E.z e. x (x i^i z) = (/)))
6	5	a1d 12	. . . . . 6 |- ((x i^i y) = (/) -> (x (_ On -> (y e. x -> E.z e. x (x i^i z) = (/))))
7		ssel 2061	. . . . . . . . 9 |- (x (_ On -> (y e. x -> y e. On))
8		visset 1811	. . . . . . . . . 10 |- y e. V
9	8	elon 2954	. . . . . . . . 9 |- (y e. On <-> Ord y)
10	7, 9	syl6ib 212	. . . . . . . 8 |- (x (_ On -> (y e. x -> Ord y))
11		inss2 2229	. . . . . . . . . . . 12 |- (x i^i y) (_ y
12		visset 1811	. . . . . . . . . . . . . 14 |- x e. V
13	12	inex1 2713	. . . . . . . . . . . . 13 |- (x i^i y) e. V
14	13	epfrc 2930	. . . . . . . . . . . 12 |- ((E Fr y /\ (x i^i y) (_ y /\ (x i^i y) =/= (/)) -> E.z e. (x i^i y)((x i^i y) i^i z) = (/))
15	11, 14	mp3an2 903	. . . . . . . . . . 11 |- ((E Fr y /\ (x i^i y) =/= (/)) -> E.z e. (x i^i y)((x i^i y) i^i z) = (/))
16	15	ex 373	. . . . . . . . . 10 |- (E Fr y -> ((x i^i y) =/= (/) -> E.z e. (x i^i y)((x i^i y) i^i z) = (/)))
17		ax-17 970	. . . . . . . . . . 11 |- (Tr y -> A.zTr y)
18		hbre1 1688	. . . . . . . . . . 11 |- (E.z e. x (x i^i z) = (/) -> A.zE.z e. x (x i^i z) = (/))
19		inss1 2228	. . . . . . . . . . . . . . . . . 18 |- (x i^i y) (_ x
20	19	sseli 2063	. . . . . . . . . . . . . . . . 17 |- (z e. (x i^i y) -> z e. x)
21		trss 2686	. . . . . . . . . . . . . . . . . . . 20 |- (Tr y -> (z e. y -> z (_ y))
22	11	sseli 2063	. . . . . . . . . . . . . . . . . . . 20 |- (z e. (x i^i y) -> z e. y)
23	21, 22	syl5 21	. . . . . . . . . . . . . . . . . . 19 |- (Tr y -> (z e. (x i^i y) -> z (_ y))
24		sseqin2 2227	. . . . . . . . . . . . . . . . . . . . . 22 |- (z (_ y <-> (y i^i z) = z)
25		ineq2 2209	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y i^i z) = z -> (x i^i (y i^i z)) = (x i^i z))
26		inass 2221	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x i^i y) i^i z) = (x i^i (y i^i z))
27	25, 26	syl5req 1519	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y i^i z) = z -> (x i^i z) = ((x i^i y) i^i z))
28	24, 27	sylbi 199	. . . . . . . . . . . . . . . . . . . . 21 |- (z (_ y -> (x i^i z) = ((x i^i y) i^i z))
29	28	eqeq1d 1482	. . . . . . . . . . . . . . . . . . . 20 |- (z (_ y -> ((x i^i z) = (/) <-> ((x i^i y) i^i z) = (/)))
30	29	biimprcd 156	. . . . . . . . . . . . . . . . . . 19 |- (((x i^i y) i^i z) = (/) -> (z (_ y -> (x i^i z) = (/)))
31	23, 30	sylan9 468	. . . . . . . . . . . . . . . . . 18 |- ((Tr y /\ ((x i^i y) i^i z) = (/)) -> (z e. (x i^i y) -> (x i^i z) = (/)))
32	31	imp 350	. . . . . . . . . . . . . . . . 17 |- (((Tr y /\ ((x i^i y) i^i z) = (/)) /\ z e. (x i^i y)) -> (x i^i z) = (/))
33	20, 32	anim12i 333	. . . . . . . . . . . . . . . 16 |- ((z e. (x i^i y) /\ ((Tr y /\ ((x i^i y) i^i z) = (/)) /\ z e. (x i^i y))) -> (z e. x /\ (x i^i z) = (/)))
34	33	exp32 377	. . . . . . . . . . . . . . 15 |- (z e. (x i^i y) -> ((Tr y /\ ((x i^i y) i^i z) = (/)) -> (z e. (x i^i y) -> (z e. x /\ (x i^i z) = (/)))))
35	34	pm2.43b 67	. . . . . . . . . . . . . 14 |- ((Tr y /\ ((x i^i y) i^i z) = (/)) -> (z e. (x i^i y) -> (z e. x /\ (x i^i z) = (/))))
36	35	ex 373	. . . . . . . . . . . . 13 |- (Tr y -> (((x i^i y) i^i z) = (/) -> (z e. (x i^i y) -> (z e. x /\ (x i^i z) = (/)))))
37	36	com23 32	. . . . . . . . . . . 12 |- (Tr y -> (z e. (x i^i y) -> (((x i^i y) i^i z) = (/) -> (z e. x /\ (x i^i z) = (/)))))
38		ra4e 1694	. . . . . . . . . . . 12 |- ((z e. x /\ (x i^i z) = (/)) -> E.z e. x (x i^i z) = (/))
39	37, 38	syl8 24	. . . . . . . . . . 11 |- (Tr y -> (z e. (x i^i y) -> (((x i^i y) i^i z) = (/) -> E.z e. x (x i^i z) = (/))))
40	17, 18, 39	r19.23ad 1744	. . . . . . . . . 10 |- (Tr y -> (E.z e. (x i^i y)((x i^i y) i^i z) = (/) -> E.z e. x (x i^i z) = (/)))
41	16, 40	sylan9 468	. . . . . . . . 9 |- ((E Fr y /\ Tr y) -> ((x i^i y) =/= (/) -> E.z e. x (x i^i z) = (/)))
42		ordfr 2960	. . . . . . . . 9 |- (Ord y -> E Fr y)
43		ordtr 2959	. . . . . . . . 9 |- (Ord y -> Tr y)
44	41, 42, 43	sylanc 471	. . . . . . . 8 |- (Ord y -> ((x i^i y) =/= (/) -> E.z e. x (x i^i z) = (/)))
45	10, 44	syl6 22	. . . . . . 7 |- (x (_ On -> (y e. x -> ((x i^i y) =/= (/) -> E.z e. x (x i^i z) = (/))))
46	45	com3r 35	. . . . . 6 |- ((x i^i y) =/= (/) -> (x (_ On -> (y e. x -> E.z e. x (x i^i z) = (/))))
47	6, 46	pm2.61ine 1633	. . . . 5 |- (x (_ On -> (y e. x -> E.z e. x (x i^i z) = (/)))
48	47	19.23adv 1214	. . . 4 |- (x (_ On -> (E.y y e. x -> E.z e. x (x i^i z) = (/)))
49		ne0 2286	. . . 4 |- (x =/= (/) <-> E.y y e. x)
50	48, 49	syl5ib 206	. . 3 |- (x (_ On -> (x =/= (/) -> E.z e. x (x i^i z) = (/)))
51	50	imp 350	. 2 |- ((x (_ On /\ x =/= (/)) -> E.z e. x (x i^i z) = (/))
52	1, 51	mpgbir 987	1 |- E Fr On

Syntax hints:   -> wi 3   /\ wa 223   = wceq 955   e. wcel 957  E.wex 979   =/= wne 1584  E.wrex 1645   i^i cin 2044   (_ wss 2045  (/)c0 2278  Tr wtr 2677  Ecep 2827   Fr wfr 2912  Ord word 2944  Oncon0 2945

This theorem is referenced by:  ordon 2984

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2700  ax-pow 2739  ax-pr 2776

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 776  df-ex 980  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1586  df-ral 1648  df-rex 1649  df-v 1810  df-dif 2047  df-un 2048  df-in 2049  df-ss 2051  df-nul 2279  df-pw 2400  df-sn 2410  df-pr 2411  df-op 2414  df-uni 2501  df-br 2617  df-opab 2664  df-tr 2678  df-eprel 2829  df-po 2837  df-so 2847  df-fr 2914  df-we 2931  df-ord 2948  df-on 2949

Copyright terms: Public domain