Theorem onfr 2992

Description: The ordinal class is founded. This lemma is needed for ordon 2993 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 2938	. 2 |- (E Fr On <-> A.x((x (_ On /\ x =/= (/)) -> E.z e. x (x i^i z) = (/)))
2		ineq2 2214	. . . . . . . . . 10 |- (z = y -> (x i^i z) = (x i^i y))
3	2	eqeq1d 1486	. . . . . . . . 9 |- (z = y -> ((x i^i z) = (/) <-> (x i^i y) = (/)))
4	3	rcla4ev 1880	. . . . . . . 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 2066	. . . . . . . . 9 |- (x (_ On -> (y e. x -> y e. On))
8		visset 1816	. . . . . . . . . 10 |- y e. V
9	8	elon 2963	. . . . . . . . 9 |- (y e. On <-> Ord y)
10	7, 9	syl6ib 212	. . . . . . . 8 |- (x (_ On -> (y e. x -> Ord y))
11		inss2 2234	. . . . . . . . . . . 12 |- (x i^i y) (_ y
12		visset 1816	. . . . . . . . . . . . . 14 |- x e. V
13	12	inex1 2721	. . . . . . . . . . . . 13 |- (x i^i y) e. V
14	13	epfrc 2939	. . . . . . . . . . . 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 906	. . . . . . . . . . 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 973	. . . . . . . . . . 11 |- (Tr y -> A.zTr y)
18		hbre1 1692	. . . . . . . . . . 11 |- (E.z e. x (x i^i z) = (/) -> A.zE.z e. x (x i^i z) = (/))
19		inss1 2233	. . . . . . . . . . . . . . . . . 18 |- (x i^i y) (_ x
20	19	sseli 2068	. . . . . . . . . . . . . . . . 17 |- (z e. (x i^i y) -> z e. x)
21		trss 2694	. . . . . . . . . . . . . . . . . . . 20 |- (Tr y -> (z e. y -> z (_ y))
22	11	sseli 2068	. . . . . . . . . . . . . . . . . . . 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 2232	. . . . . . . . . . . . . . . . . . . . . 22 |- (z (_ y <-> (y i^i z) = z)
25		ineq2 2214	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y i^i z) = z -> (x i^i (y i^i z)) = (x i^i z))
26		inass 2226	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x i^i y) i^i z) = (x i^i (y i^i z))
27	25, 26	syl5req 1523	. . . . . . . . . . . . . . . . . . . . . 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 1486	. . . . . . . . . . . . . . . . . . . 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 470	. . . . . . . . . . . . . . . . . 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 379	. . . . . . . . . . . . . . 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 1698	. . . . . . . . . . . 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 1748	. . . . . . . . . 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 470	. . . . . . . . 9 |- ((E Fr y /\ Tr y) -> ((x i^i y) =/= (/) -> E.z e. x (x i^i z) = (/)))
42		ordfr 2969	. . . . . . . . 9 |- (Ord y -> E Fr y)
43		ordtr 2968	. . . . . . . . 9 |- (Ord y -> Tr y)
44	41, 42, 43	sylanc 473	. . . . . . . 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 1637	. . . . 5 |- (x (_ On -> (y e. x -> E.z e. x (x i^i z) = (/)))
48	47	19.23adv 1216	. . . 4 |- (x (_ On -> (E.y y e. x -> E.z e. x (x i^i z) = (/)))
49		ne0 2292	. . . 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 990	1 |- E Fr On

Syntax hints:   -> wi 3   /\ wa 223   = wceq 958   e. wcel 960  E.wex 982   =/= wne 1588  E.wrex 1649   i^i cin 2049   (_ wss 2050  (/)c0 2283  Tr wtr 2685  Ecep 2836   Fr wfr 2921  Ord word 2953  Oncon0 2954

This theorem is referenced by:  ordon 2993

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2708  ax-pow 2748  ax-pr 2785

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-v 1815  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417  df-op 2420  df-uni 2508  df-br 2625  df-opab 2672  df-tr 2686  df-eprel 2838  df-po 2846  df-so 2856  df-fr 2923  df-we 2940  df-ord 2957  df-on 2958

Copyright terms: Public domain