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