Metamath Proof Explorer


Theorem dfon2lem9

Description: Lemma for dfon2 . A class of new ordinals is well-founded by _E . (Contributed by Scott Fenton, 3-Mar-2011)

Ref Expression
Assertion dfon2lem9 x A y y x Tr y y x E Fr A

Proof

Step Hyp Ref Expression
1 ssralv z A x A y y x Tr y y x x z y y x Tr y y x
2 dfon2lem8 z x z y y x Tr y y x u u z Tr u u z z z
3 2 simprd z x z y y x Tr y y x z z
4 intss1 t z z t
5 2 simpld z x z y y x Tr y y x u u z Tr u u z
6 intex z z V
7 dfon2lem3 z V u u z Tr u u z Tr z x z ¬ x x
8 7 imp z V u u z Tr u u z Tr z x z ¬ x x
9 8 simprd z V u u z Tr u u z x z ¬ x x
10 untelirr x z ¬ x x ¬ z z
11 9 10 syl z V u u z Tr u u z ¬ z z
12 eleq1 z = t z z t z
13 12 notbid z = t ¬ z z ¬ t z
14 11 13 syl5ibcom z V u u z Tr u u z z = t ¬ t z
15 14 a1dd z V u u z Tr u u z z = t z t ¬ t z
16 8 simpld z V u u z Tr u u z Tr z
17 trss Tr z t z t z
18 16 17 syl z V u u z Tr u u z t z t z
19 eqss z = t z t t z
20 19 simplbi2com t z z t z = t
21 18 20 syl6 z V u u z Tr u u z t z z t z = t
22 21 com23 z V u u z Tr u u z z t t z z = t
23 con3 t z z = t ¬ z = t ¬ t z
24 22 23 syl6 z V u u z Tr u u z z t ¬ z = t ¬ t z
25 24 com23 z V u u z Tr u u z ¬ z = t z t ¬ t z
26 15 25 pm2.61d z V u u z Tr u u z z t ¬ t z
27 6 26 sylanb z u u z Tr u u z z t ¬ t z
28 5 27 syldan z x z y y x Tr y y x z t ¬ t z
29 4 28 syl5 z x z y y x Tr y y x t z ¬ t z
30 29 ralrimiv z x z y y x Tr y y x t z ¬ t z
31 eleq2 w = z t w t z
32 31 notbid w = z ¬ t w ¬ t z
33 32 ralbidv w = z t z ¬ t w t z ¬ t z
34 33 rspcev z z t z ¬ t z w z t z ¬ t w
35 3 30 34 syl2anc z x z y y x Tr y y x w z t z ¬ t w
36 35 expcom x z y y x Tr y y x z w z t z ¬ t w
37 1 36 syl6com x A y y x Tr y y x z A z w z t z ¬ t w
38 37 impd x A y y x Tr y y x z A z w z t z ¬ t w
39 38 alrimiv x A y y x Tr y y x z z A z w z t z ¬ t w
40 df-fr E Fr A z z A z w z t z ¬ t E w
41 epel t E w t w
42 41 notbii ¬ t E w ¬ t w
43 42 ralbii t z ¬ t E w t z ¬ t w
44 43 rexbii w z t z ¬ t E w w z t z ¬ t w
45 44 imbi2i z A z w z t z ¬ t E w z A z w z t z ¬ t w
46 45 albii z z A z w z t z ¬ t E w z z A z w z t z ¬ t w
47 40 46 bitri E Fr A z z A z w z t z ¬ t w
48 39 47 sylibr x A y y x Tr y y x E Fr A