Metamath Proof Explorer


Theorem aomclem4

Description: Lemma for dfac11 . Limit case. Patch together well-orderings constructed so far using fnwe2 to cover the limit rank. (Contributed by Stefan O'Rear, 20-Jan-2015)

Ref Expression
Hypotheses aomclem4.f F = a b | rank a E rank b rank a = rank b a z suc rank a b
aomclem4.on φ dom z On
aomclem4.su φ dom z = dom z
aomclem4.we φ a dom z z a We R1 a
Assertion aomclem4 φ F We R1 dom z

Proof

Step Hyp Ref Expression
1 aomclem4.f F = a b | rank a E rank b rank a = rank b a z suc rank a b
2 aomclem4.on φ dom z On
3 aomclem4.su φ dom z = dom z
4 aomclem4.we φ a dom z z a We R1 a
5 suceq c = rank a suc c = suc rank a
6 5 fveq2d c = rank a z suc c = z suc rank a
7 r1fnon R1 Fn On
8 fnfun R1 Fn On Fun R1
9 7 8 ax-mp Fun R1
10 fndm R1 Fn On dom R1 = On
11 7 10 ax-mp dom R1 = On
12 11 eqimss2i On dom R1
13 9 12 pm3.2i Fun R1 On dom R1
14 funfvima2 Fun R1 On dom R1 dom z On R1 dom z R1 On
15 13 2 14 mpsyl φ R1 dom z R1 On
16 elssuni R1 dom z R1 On R1 dom z R1 On
17 15 16 syl φ R1 dom z R1 On
18 17 sselda φ b R1 dom z b R1 On
19 rankidb b R1 On b R1 suc rank b
20 18 19 syl φ b R1 dom z b R1 suc rank b
21 suceq rank b = rank a suc rank b = suc rank a
22 21 fveq2d rank b = rank a R1 suc rank b = R1 suc rank a
23 22 eleq2d rank b = rank a b R1 suc rank b b R1 suc rank a
24 20 23 syl5ibcom φ b R1 dom z rank b = rank a b R1 suc rank a
25 24 expimpd φ b R1 dom z rank b = rank a b R1 suc rank a
26 25 ss2abdv φ b | b R1 dom z rank b = rank a b | b R1 suc rank a
27 df-rab b R1 dom z | rank b = rank a = b | b R1 dom z rank b = rank a
28 abid1 R1 suc rank a = b | b R1 suc rank a
29 26 27 28 3sstr4g φ b R1 dom z | rank b = rank a R1 suc rank a
30 29 adantr φ a R1 dom z b R1 dom z | rank b = rank a R1 suc rank a
31 fveq2 b = suc rank a z b = z suc rank a
32 fveq2 b = suc rank a R1 b = R1 suc rank a
33 31 32 weeq12d b = suc rank a z b We R1 b z suc rank a We R1 suc rank a
34 fveq2 a = b z a = z b
35 fveq2 a = b R1 a = R1 b
36 34 35 weeq12d a = b z a We R1 a z b We R1 b
37 36 cbvralvw a dom z z a We R1 a b dom z z b We R1 b
38 4 37 sylib φ b dom z z b We R1 b
39 38 adantr φ a R1 dom z b dom z z b We R1 b
40 rankr1ai a R1 dom z rank a dom z
41 40 adantl φ a R1 dom z rank a dom z
42 eloni dom z On Ord dom z
43 2 42 syl φ Ord dom z
44 limsuc2 Ord dom z dom z = dom z rank a dom z suc rank a dom z
45 43 3 44 syl2anc φ rank a dom z suc rank a dom z
46 45 adantr φ a R1 dom z rank a dom z suc rank a dom z
47 41 46 mpbid φ a R1 dom z suc rank a dom z
48 33 39 47 rspcdva φ a R1 dom z z suc rank a We R1 suc rank a
49 wess b R1 dom z | rank b = rank a R1 suc rank a z suc rank a We R1 suc rank a z suc rank a We b R1 dom z | rank b = rank a
50 30 48 49 sylc φ a R1 dom z z suc rank a We b R1 dom z | rank b = rank a
51 rankf rank : R1 On On
52 51 a1i φ rank : R1 On On
53 52 17 fssresd φ rank R1 dom z : R1 dom z On
54 epweon E We On
55 54 a1i φ E We On
56 6 1 50 53 55 fnwe2 φ F We R1 dom z