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		r1fun	⊢ Fun 𝑅1
6		funiunfv	⊢ ( Fun 𝑅1 → ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = ∪ ( 𝑅1 “ On ) )
7	5 6	ax-mp	⊢ ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = ∪ ( 𝑅1 “ On )
8		treq	⊢ ( ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = ∪ ( 𝑅1 “ On ) → ( Tr ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) ↔ Tr ∪ ( 𝑅1 “ On ) ) )
9	7 8	ax-mp	⊢ ( Tr ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) ↔ Tr ∪ ( 𝑅1 “ On ) )
10	4 9	mpbi	⊢ Tr ∪ ( 𝑅1 “ On )
11		trss	⊢ ( Tr ∪ ( 𝑅1 “ On ) → ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ∪ ( 𝑅1 “ On ) ) )
12	10 11	ax-mp	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )