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

Metamath Proof Explorer

Theorem rankr1ai

Description: One direction of rankr1a . (Contributed by Mario Carneiro, 28-May-2013) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion rankr1ai ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( rank ‘ 𝐴 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐵 ∈ dom 𝑅1 )
2 r1val1 ⊢ ( 𝐵 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 𝒫 ( 𝑅1 ‘ 𝑥 ) )
3 2 eleq2d ⊢ ( 𝐵 ∈ dom 𝑅1 → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ 𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝒫 ( 𝑅1 ‘ 𝑥 ) ) )
4 eliun ⊢ ( 𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝒫 ( 𝑅1 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐵 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) )
5 3 4 bitrdi ⊢ ( 𝐵 ∈ dom 𝑅1 → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐵 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) ) )
6 r1funlim ⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
7 6 simpri ⊢ Lim dom 𝑅1
8 limord ⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
9 7 8 ax-mp ⊢ Ord dom 𝑅1
10 ordtr1 ⊢ ( Ord dom 𝑅1 → ( ( 𝑥 ∈ 𝐵 ∧ 𝐵 ∈ dom 𝑅1 ) → 𝑥 ∈ dom 𝑅1 ) )
11 9 10 ax-mp ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝐵 ∈ dom 𝑅1 ) → 𝑥 ∈ dom 𝑅1 )
12 11 ancoms ⊢ ( ( 𝐵 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ dom 𝑅1 )
13 r1sucg ⊢ ( 𝑥 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝑥 ) = 𝒫 ( 𝑅1 ‘ 𝑥 ) )
14 13 eleq2d ⊢ ( 𝑥 ∈ dom 𝑅1 → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ↔ 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) ) )
15 12 14 syl ⊢ ( ( 𝐵 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ↔ 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) ) )
16 ordsson ⊢ ( Ord dom 𝑅1 → dom 𝑅1 ⊆ On )
17 9 16 ax-mp ⊢ dom 𝑅1 ⊆ On
18 17 12 sselid ⊢ ( ( 𝐵 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ On )
19 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ↔ ( 𝑥 ∈ On ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ) )
20 intss1 ⊢ ( 𝑥 ∈ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } → ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 )
21 19 20 sylbir ⊢ ( ( 𝑥 ∈ On ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ) → ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 )
22 18 21 sylan ⊢ ( ( ( 𝐵 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ) → ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 )
23 22 ex ⊢ ( ( 𝐵 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 ) )
24 15 23 sylbird ⊢ ( ( 𝐵 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) → ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 ) )
25 24 reximdva ⊢ ( 𝐵 ∈ dom 𝑅1 → ( ∃ 𝑥 ∈ 𝐵 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) → ∃ 𝑥 ∈ 𝐵 ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 ) )
26 5 25 sylbid ⊢ ( 𝐵 ∈ dom 𝑅1 → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 ) )
27 1 26 mpcom ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 )
28 r1elwf ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
29 rankvalb ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )
30 28 29 syl ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )
31 30 sseq1d ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( ( rank ‘ 𝐴 ) ⊆ 𝑥 ↔ ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 ) )
32 31 adantr ⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( rank ‘ 𝐴 ) ⊆ 𝑥 ↔ ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 ) )
33 rankon ⊢ ( rank ‘ 𝐴 ) ∈ On
34 17 1 sselid ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐵 ∈ On )
35 ontr2 ⊢ ( ( ( rank ‘ 𝐴 ) ∈ On ∧ 𝐵 ∈ On ) → ( ( ( rank ‘ 𝐴 ) ⊆ 𝑥 ∧ 𝑥 ∈ 𝐵 ) → ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
36 33 34 35 sylancr ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( ( ( rank ‘ 𝐴 ) ⊆ 𝑥 ∧ 𝑥 ∈ 𝐵 ) → ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
37 36 expcomd ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( 𝑥 ∈ 𝐵 → ( ( rank ‘ 𝐴 ) ⊆ 𝑥 → ( rank ‘ 𝐴 ) ∈ 𝐵 ) ) )
38 37 imp ⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( rank ‘ 𝐴 ) ⊆ 𝑥 → ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
39 32 38 sylbird ⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 → ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
40 39 rexlimdva ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( ∃ 𝑥 ∈ 𝐵 ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ⊆ 𝑥 → ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
41 27 40 mpd ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( rank ‘ 𝐴 ) ∈ 𝐵 )