This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( rank ‘ 𝑎 ) E ( rank ‘ 𝑏 ) ∨ ( ( rank ‘ 𝑎 ) = ( rank ‘ 𝑏 ) ∧ 𝑎 ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) 𝑏 ) ) }
aomclem4.on ⊢ ( 𝜑 → dom 𝑧 ∈ On )
aomclem4.su ⊢ ( 𝜑 → dom 𝑧 = ∪ dom 𝑧 )
aomclem4.we ⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
Assertion aomclem4 ( 𝜑 → 𝐹 We ( 𝑅1 ‘ dom 𝑧 ) )

Proof

Step Hyp Ref Expression
1 aomclem4.f ⊢ 𝐹 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( rank ‘ 𝑎 ) E ( rank ‘ 𝑏 ) ∨ ( ( rank ‘ 𝑎 ) = ( rank ‘ 𝑏 ) ∧ 𝑎 ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) 𝑏 ) ) }
2 aomclem4.on ⊢ ( 𝜑 → dom 𝑧 ∈ On )
3 aomclem4.su ⊢ ( 𝜑 → dom 𝑧 = ∪ dom 𝑧 )
4 aomclem4.we ⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
5 suceq ⊢ ( 𝑐 = ( rank ‘ 𝑎 ) → suc 𝑐 = suc ( rank ‘ 𝑎 ) )
6 5 fveq2d ⊢ ( 𝑐 = ( rank ‘ 𝑎 ) → ( 𝑧 ‘ suc 𝑐 ) = ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) )
7 r1fnon ⊢ 𝑅1 Fn On
8 fnfun ⊢ ( 𝑅1 Fn On → Fun 𝑅1 )
9 7 8 ax-mp ⊢ Fun 𝑅1
10 7 fndmi ⊢ dom 𝑅1 = On
11 10 eqimss2i ⊢ On ⊆ dom 𝑅1
12 9 11 pm3.2i ⊢ ( Fun 𝑅1 ∧ On ⊆ dom 𝑅1 )
13 funfvima2 ⊢ ( ( Fun 𝑅1 ∧ On ⊆ dom 𝑅1 ) → ( dom 𝑧 ∈ On → ( 𝑅1 ‘ dom 𝑧 ) ∈ ( 𝑅1 “ On ) ) )
14 12 2 13 mpsyl ⊢ ( 𝜑 → ( 𝑅1 ‘ dom 𝑧 ) ∈ ( 𝑅1 “ On ) )
15 elssuni ⊢ ( ( 𝑅1 ‘ dom 𝑧 ) ∈ ( 𝑅1 “ On ) → ( 𝑅1 ‘ dom 𝑧 ) ⊆ ∪ ( 𝑅1 “ On ) )
16 14 15 syl ⊢ ( 𝜑 → ( 𝑅1 ‘ dom 𝑧 ) ⊆ ∪ ( 𝑅1 “ On ) )
17 16 sselda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → 𝑏 ∈ ∪ ( 𝑅1 “ On ) )
18 rankidb ⊢ ( 𝑏 ∈ ∪ ( 𝑅1 “ On ) → 𝑏 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑏 ) ) )
19 17 18 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → 𝑏 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑏 ) ) )
20 suceq ⊢ ( ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) → suc ( rank ‘ 𝑏 ) = suc ( rank ‘ 𝑎 ) )
21 20 fveq2d ⊢ ( ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) → ( 𝑅1 ‘ suc ( rank ‘ 𝑏 ) ) = ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) )
22 21 eleq2d ⊢ ( ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) → ( 𝑏 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑏 ) ) ↔ 𝑏 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) ) )
23 19 22 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → ( ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) → 𝑏 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) ) )
24 23 expimpd ⊢ ( 𝜑 → ( ( 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ∧ ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) ) → 𝑏 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) ) )
25 24 ss2abdv ⊢ ( 𝜑 → { 𝑏 ∣ ( 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ∧ ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) ) } ⊆ { 𝑏 ∣ 𝑏 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) } )
26 df-rab ⊢ { 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ∣ ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) } = { 𝑏 ∣ ( 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ∧ ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) ) }
27 abid1 ⊢ ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) = { 𝑏 ∣ 𝑏 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) }
28 25 26 27 3sstr4g ⊢ ( 𝜑 → { 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ∣ ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) } ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → { 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ∣ ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) } ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) )
30 fveq2 ⊢ ( 𝑏 = suc ( rank ‘ 𝑎 ) → ( 𝑧 ‘ 𝑏 ) = ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) )
31 fveq2 ⊢ ( 𝑏 = suc ( rank ‘ 𝑎 ) → ( 𝑅1 ‘ 𝑏 ) = ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) )
32 30 31 weeq12d ⊢ ( 𝑏 = suc ( rank ‘ 𝑎 ) → ( ( 𝑧 ‘ 𝑏 ) We ( 𝑅1 ‘ 𝑏 ) ↔ ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) ) )
33 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝑧 ‘ 𝑎 ) = ( 𝑧 ‘ 𝑏 ) )
34 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝑅1 ‘ 𝑎 ) = ( 𝑅1 ‘ 𝑏 ) )
35 33 34 weeq12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ↔ ( 𝑧 ‘ 𝑏 ) We ( 𝑅1 ‘ 𝑏 ) ) )
36 35 cbvralvw ⊢ ( ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) ↔ ∀ 𝑏 ∈ dom 𝑧 ( 𝑧 ‘ 𝑏 ) We ( 𝑅1 ‘ 𝑏 ) )
37 4 36 sylib ⊢ ( 𝜑 → ∀ 𝑏 ∈ dom 𝑧 ( 𝑧 ‘ 𝑏 ) We ( 𝑅1 ‘ 𝑏 ) )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → ∀ 𝑏 ∈ dom 𝑧 ( 𝑧 ‘ 𝑏 ) We ( 𝑅1 ‘ 𝑏 ) )
39 rankr1ai ⊢ ( 𝑎 ∈ ( 𝑅1 ‘ dom 𝑧 ) → ( rank ‘ 𝑎 ) ∈ dom 𝑧 )
40 39 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → ( rank ‘ 𝑎 ) ∈ dom 𝑧 )
41 eloni ⊢ ( dom 𝑧 ∈ On → Ord dom 𝑧 )
42 2 41 syl ⊢ ( 𝜑 → Ord dom 𝑧 )
43 limsuc2 ⊢ ( ( Ord dom 𝑧 ∧ dom 𝑧 = ∪ dom 𝑧 ) → ( ( rank ‘ 𝑎 ) ∈ dom 𝑧 ↔ suc ( rank ‘ 𝑎 ) ∈ dom 𝑧 ) )
44 42 3 43 syl2anc ⊢ ( 𝜑 → ( ( rank ‘ 𝑎 ) ∈ dom 𝑧 ↔ suc ( rank ‘ 𝑎 ) ∈ dom 𝑧 ) )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → ( ( rank ‘ 𝑎 ) ∈ dom 𝑧 ↔ suc ( rank ‘ 𝑎 ) ∈ dom 𝑧 ) )
46 40 45 mpbid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → suc ( rank ‘ 𝑎 ) ∈ dom 𝑧 )
47 32 38 46 rspcdva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) )
48 wess ⊢ ( { 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ∣ ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) } ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) → ( ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑎 ) ) → ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) We { 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ∣ ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) } ) )
49 29 47 48 sylc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑅1 ‘ dom 𝑧 ) ) → ( 𝑧 ‘ suc ( rank ‘ 𝑎 ) ) We { 𝑏 ∈ ( 𝑅1 ‘ dom 𝑧 ) ∣ ( rank ‘ 𝑏 ) = ( rank ‘ 𝑎 ) } )
50 rankf ⊢ rank : ∪ ( 𝑅1 “ On ) ⟶ On
51 50 a1i ⊢ ( 𝜑 → rank : ∪ ( 𝑅1 “ On ) ⟶ On )
52 51 16 fssresd ⊢ ( 𝜑 → ( rank ↾ ( 𝑅1 ‘ dom 𝑧 ) ) : ( 𝑅1 ‘ dom 𝑧 ) ⟶ On )
53 epweon ⊢ E We On
54 53 a1i ⊢ ( 𝜑 → E We On )
55 6 1 49 52 54 fnwe2 ⊢ ( 𝜑 → 𝐹 We ( 𝑅1 ‘ dom 𝑧 ) )