Theorem r1elssi

Description: The range of the R1 function is transitive. Lemma 2.10 of Kunen p. 97. One direction of r1elss that doesn't need A to be a set. (Contributed by Mario Carneiro, 22-Mar-2013) (Revised by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Assertion	r1elssi	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )

Proof

Step	Hyp	Ref	Expression
1		triun	⊢ ( ∀ 𝑥 ∈ On Tr ( 𝑅1 ‘ 𝑥 ) → Tr ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) )
2		r1tr	⊢ Tr ( 𝑅1 ‘ 𝑥 )
3	2	a1i	⊢ ( 𝑥 ∈ On → Tr ( 𝑅1 ‘ 𝑥 ) )
4	1 3	mprg	⊢ Tr ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 )
5		r1funlim	⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
6	5	simpli	⊢ Fun 𝑅1
7		funiunfv	⊢ ( Fun 𝑅1 → ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = ∪ ( 𝑅1 “ On ) )
8	6 7	ax-mp	⊢ ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = ∪ ( 𝑅1 “ On )
9		treq	⊢ ( ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = ∪ ( 𝑅1 “ On ) → ( Tr ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) ↔ Tr ∪ ( 𝑅1 “ On ) ) )
10	8 9	ax-mp	⊢ ( Tr ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) ↔ Tr ∪ ( 𝑅1 “ On ) )
11	4 10	mpbi	⊢ Tr ∪ ( 𝑅1 “ On )
12		trss	⊢ ( Tr ∪ ( 𝑅1 “ On ) → ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ∪ ( 𝑅1 “ On ) ) )
13	11 12	ax-mp	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )