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

Metamath Proof Explorer

Theorem r1elwf

Description: Any member of the cumulative hierarchy is well-founded. (Contributed by Mario Carneiro, 28-May-2013) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion r1elwf ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )

Proof

Step Hyp Ref Expression
1 r1funlim ⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
2 1 simpri ⊢ Lim dom 𝑅1
3 limord ⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
4 ordsson ⊢ ( Ord dom 𝑅1 → dom 𝑅1 ⊆ On )
5 2 3 4 mp2b ⊢ dom 𝑅1 ⊆ On
6 elfvdm ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐵 ∈ dom 𝑅1 )
7 5 6 sselid ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐵 ∈ On )
8 r1tr ⊢ Tr ( 𝑅1 ‘ 𝐵 )
9 trss ⊢ ( Tr ( 𝑅1 ‘ 𝐵 ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) ) )
10 8 9 ax-mp ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) )
11 elpwg ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝐵 ) ↔ 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) ) )
12 10 11 mpbird ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝐵 ) )
13 r1sucg ⊢ ( 𝐵 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝐵 ) = 𝒫 ( 𝑅1 ‘ 𝐵 ) )
14 6 13 syl ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( 𝑅1 ‘ suc 𝐵 ) = 𝒫 ( 𝑅1 ‘ 𝐵 ) )
15 12 14 eleqtrrd ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) )
16 suceq ⊢ ( 𝑥 = 𝐵 → suc 𝑥 = suc 𝐵 )
17 16 fveq2d ⊢ ( 𝑥 = 𝐵 → ( 𝑅1 ‘ suc 𝑥 ) = ( 𝑅1 ‘ suc 𝐵 ) )
18 17 eleq2d ⊢ ( 𝑥 = 𝐵 → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ↔ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) )
19 18 rspcev ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
20 7 15 19 syl2anc ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
21 rankwflemb ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
22 20 21 sylibr ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )