Theorem r1elwf

Description: Any element of (any stage of) the cumulative hierarchy of sets is well-founded (recall that U. ( R1 " On ) is the class of well-founded sets). (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		r1dmlim	⊢ Lim dom 𝑅1
2		limord	⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
3		ordsson	⊢ ( Ord dom 𝑅1 → dom 𝑅1 ⊆ On )
4	1 2 3	mp2b	⊢ dom 𝑅1 ⊆ On
5		elfvdm	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐵 ∈ dom 𝑅1 )
6	4 5	sselid	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐵 ∈ On )
7		r1tr	⊢ Tr ( 𝑅1 ‘ 𝐵 )
8		trss	⊢ ( Tr ( 𝑅1 ‘ 𝐵 ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) ) )
9	7 8	ax-mp	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) )
10		elpwg	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝐵 ) ↔ 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) ) )
11	9 10	mpbird	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝐵 ) )
12		r1sucg	⊢ ( 𝐵 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝐵 ) = 𝒫 ( 𝑅1 ‘ 𝐵 ) )
13	5 12	syl	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( 𝑅1 ‘ suc 𝐵 ) = 𝒫 ( 𝑅1 ‘ 𝐵 ) )
14	11 13	eleqtrrd	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) )
15		suceq	⊢ ( 𝑥 = 𝐵 → suc 𝑥 = suc 𝐵 )
16	15	fveq2d	⊢ ( 𝑥 = 𝐵 → ( 𝑅1 ‘ suc 𝑥 ) = ( 𝑅1 ‘ suc 𝐵 ) )
17	16	eleq2d	⊢ ( 𝑥 = 𝐵 → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ↔ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) )
18	17	rspcev	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
19	6 14 18	syl2anc	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
20		rankwflemb	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
21	19 20	sylibr	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )