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	sseldi	⊢ ( 𝐴 ∈ ( 𝑅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 ) )