Theorem dfon2lem9 13857

Description: Lemma for dfon2 13858. A class of new ordinals is well-founded by _E.

Assertion

Ref	Expression
dfon2lem9	|- (A.x e. A A.y((y C. x /\ Tr y) -> y e. x) -> _E Fr A)

Distinct variable group:   x,A,y

Proof of Theorem dfon2lem9

Step	Hyp	Ref	Expression
1		ssralv 2672	. . . . 5 |- (z C_ A -> (A.x e. A A.y((y C. x /\ Tr y) -> y e. x) -> A.x e. z A.y((y C. x /\ Tr y) -> y e. x)))
2		dfon2lem8 13856	. . . . . . . 8 |- ((z =/= (/) /\ A.x e. z A.y((y C. x /\ Tr y) -> y e. x)) -> (A.u((u C. |^|z /\ Tr u) -> u e. |^|z) /\ |^|z e. z))
3	2	simprd 352	. . . . . . 7 |- ((z =/= (/) /\ A.x e. z A.y((y C. x /\ Tr y) -> y e. x)) -> |^|z e. z)
4	2	simplld 348	. . . . . . . . . 10 |- ((z =/= (/) /\ A.x e. z A.y((y C. x /\ Tr y) -> y e. x)) -> A.u((u C. |^|z /\ Tr u) -> u e. |^|z))
5		eleq1 1957	. . . . . . . . . . . . . . 15 |- (|^|z = t -> (|^|z e. |^|z <-> t e. |^|z))
6	5	notbid 673	. . . . . . . . . . . . . 14 |- (|^|z = t -> (-. |^|z e. |^|z <-> -. t e. |^|z))
7		dfon2lem3 13851	. . . . . . . . . . . . . . . . 17 |- (|^|z e. _V -> (A.u((u C. |^|z /\ Tr u) -> u e. |^|z) -> (Tr |^|z /\ A.x e. |^|z -. x e. x)))
8	7	imp 377	. . . . . . . . . . . . . . . 16 |- ((|^|z e. _V /\ A.u((u C. |^|z /\ Tr u) -> u e. |^|z)) -> (Tr |^|z /\ A.x e. |^|z -. x e. x))
9	8	simprd 352	. . . . . . . . . . . . . . 15 |- ((|^|z e. _V /\ A.u((u C. |^|z /\ Tr u) -> u e. |^|z)) -> A.x e. |^|z -. x e. x)
10		untelirr 13796	. . . . . . . . . . . . . . 15 |- (A.x e. |^|z -. x e. x -> -. |^|z e. |^|z)
11	9, 10	syl 12	. . . . . . . . . . . . . 14 |- ((|^|z e. _V /\ A.u((u C. |^|z /\ Tr u) -> u e. |^|z)) -> -. |^|z e. |^|z)
12	6, 11	syl5cbi 226	. . . . . . . . . . . . 13 |- ((|^|z e. _V /\ A.u((u C. |^|z /\ Tr u) -> u e. |^|z)) -> (|^|z = t -> -. t e. |^|z))
13	12	a1dd 53	. . . . . . . . . . . 12 |- ((|^|z e. _V /\ A.u((u C. |^|z /\ Tr u) -> u e. |^|z)) -> (|^|z = t -> (|^|z C_ t -> -. t e. |^|z)))
14	8	simplld 348	. . . . . . . . . . . . . . . . 17 |- ((|^|z e. _V /\ A.u((u C. |^|z /\ Tr u) -> u e. |^|z)) -> Tr |^|z)
15		trss 3421	. . . . . . . . . . . . . . . . 17 |- (Tr |^|z -> (t e. |^|z -> t C_ |^|z))
16	14, 15	syl 12	. . . . . . . . . . . . . . . 16 |- ((|^|z e. _V /\ A.u((u C. |^|z /\ Tr u) -> u e. |^|z)) -> (t e. |^|z -> t C_ |^|z))
17		eqss 2631	. . . . . . . . . . . . . . . . . 18 |- (|^|z = t <-> (|^|z C_ t /\ t C_ |^|z))
18	17	biimpri 169	. . . . . . . . . . . . . . . . 17 |- ((|^|z C_ t /\ t C_ |^|z) -> |^|z = t)
19	18	expcom 403	. . . . . . . . . . . . . . . 16 |- (t C_ |^|z -> (|^|z C_ t -> |^|z = t))
20	16, 19	syl6 25	. . . . . . . . . . . . . . 15 |- ((|^|z e. _V /\ A.u((u C. |^|z /\ Tr u) -> u e. |^|z)) -> (t e. |^|z -> (|^|z C_ t -> |^|z = t)))
21	20	com23 36	. . . . . . . . . . . . . 14 |- ((|^|z e. _V /\ A.u((u C. |^|z /\ Tr u) -> u e. |^|z)) -> (|^|z C_ t -> (t e. |^|z -> |^|z = t)))
22		con3 110	. . . . . . . . . . . . . 14 |- ((t e. |^|z -> |^|z = t) -> (-. |^|z = t -> -. t e. |^|z))
23	21, 22	syl6 25	. . . . . . . . . . . . 13 |- ((|^|z e. _V /\ A.u((u C. |^|z /\ Tr u) -> u e. |^|z)) -> (|^|z C_ t -> (-. |^|z = t -> -. t e. |^|z)))
24	23	com23 36	. . . . . . . . . . . 12 |- ((|^|z e. _V /\ A.u((u C. |^|z /\ Tr u) -> u e. |^|z)) -> (-. |^|z = t -> (|^|z C_ t -> -. t e. |^|z)))
25	13, 24	pm2.61d 141	. . . . . . . . . . 11 |- ((|^|z e. _V /\ A.u((u C. |^|z /\ Tr u) -> u e. |^|z)) -> (|^|z C_ t -> -. t e. |^|z))
26		intex 3465	. . . . . . . . . . 11 |- (z =/= (/) <-> |^|z e. _V)
27	25, 26	sylanb 498	. . . . . . . . . 10 |- ((z =/= (/) /\ A.u((u C. |^|z /\ Tr u) -> u e. |^|z)) -> (|^|z C_ t -> -. t e. |^|z))
28	4, 27	syldan 516	. . . . . . . . 9 |- ((z =/= (/) /\ A.x e. z A.y((y C. x /\ Tr y) -> y e. x)) -> (|^|z C_ t -> -. t e. |^|z))
29		intss1 3231	. . . . . . . . 9 |- (t e. z -> |^|z C_ t)
30	28, 29	syl5 20	. . . . . . . 8 |- ((z =/= (/) /\ A.x e. z A.y((y C. x /\ Tr y) -> y e. x)) -> (t e. z -> -. t e. |^|z))
31	30	r19.21aiv 2175	. . . . . . 7 |- ((z =/= (/) /\ A.x e. z A.y((y C. x /\ Tr y) -> y e. x)) -> A.t e. z -. t e. |^|z)
32		eleq2 1958	. . . . . . . . . 10 |- (w = |^|z -> (t e. w <-> t e. |^|z))
33	32	notbid 673	. . . . . . . . 9 |- (w = |^|z -> (-. t e. w <-> -. t e. |^|z))
34	33	ralbidv 2123	. . . . . . . 8 |- (w = |^|z -> (A.t e. z -. t e. w <-> A.t e. z -. t e. |^|z))
35	34	rcla4ev 2381	. . . . . . 7 |- ((|^|z e. z /\ A.t e. z -. t e. |^|z) -> E.w e. z A.t e. z -. t e. w)
36	3, 31, 35	syl11anc 524	. . . . . 6 |- ((z =/= (/) /\ A.x e. z A.y((y C. x /\ Tr y) -> y e. x)) -> E.w e. z A.t e. z -. t e. w)
37	36	expcom 403	. . . . 5 |- (A.x e. z A.y((y C. x /\ Tr y) -> y e. x) -> (z =/= (/) -> E.w e. z A.t e. z -. t e. w))
38	1, 37	syl6com 64	. . . 4 |- (A.x e. A A.y((y C. x /\ Tr y) -> y e. x) -> (z C_ A -> (z =/= (/) -> E.w e. z A.t e. z -. t e. w)))
39	38	imp3a 388	. . 3 |- (A.x e. A A.y((y C. x /\ Tr y) -> y e. x) -> ((z C_ A /\ z =/= (/)) -> E.w e. z A.t e. z -. t e. w))
40	39	19.21aiv 1664	. 2 |- (A.x e. A A.y((y C. x /\ Tr y) -> y e. x) -> A.z((z C_ A /\ z =/= (/)) -> E.w e. z A.t e. z -. t e. w))
41		df-fr 3625	. . 3 |- ( _E Fr A <-> A.z((z C_ A /\ z =/= (/)) -> E.w e. z A.t e. z -. t _E w))
42		epel 3585	. . . . . . . 8 |- (t _E w <-> t e. w)
43	42	notbii 204	. . . . . . 7 |- (-. t _E w <-> -. t e. w)
44	43	ralbii 2127	. . . . . 6 |- (A.t e. z -. t _E w <-> A.t e. z -. t e. w)
45	44	rexbii 2128	. . . . 5 |- (E.w e. z A.t e. z -. t _E w <-> E.w e. z A.t e. z -. t e. w)
46	45	imbi2i 202	. . . 4 |- (((z C_ A /\ z =/= (/)) -> E.w e. z A.t e. z -. t _E w) <-> ((z C_ A /\ z =/= (/)) -> E.w e. z A.t e. z -. t e. w))
47	46	albii 1346	. . 3 |- (A.z((z C_ A /\ z =/= (/)) -> E.w e. z A.t e. z -. t _E w) <-> A.z((z C_ A /\ z =/= (/)) -> E.w e. z A.t e. z -. t e. w))
48	41, 47	bitri 190	. 2 |- ( _E Fr A <-> A.z((z C_ A /\ z =/= (/)) -> E.w e. z A.t e. z -. t e. w))
49	40, 48	sylibr 217	1 |- (A.x e. A A.y((y C. x /\ Tr y) -> y e. x) -> _E Fr A)

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   C_ wss 2593   C. wpss 2594  (/)c0 2875  |^|cint 3214   class class class wbr 3338  Tr wtr 3411   _E cep 3581   Fr wfr 3623

This theorem is referenced by:  dfon2 13858

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-int 3215  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-fr 3625  df-suc 3663

Copyright terms: Public domain