Theorem r1elss

Description: The range of the R1 function is transitive. Lemma 2.10 of Kunen p. 97. (Contributed by Mario Carneiro, 22-Mar-2013) (Revised by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Hypothesis	r1elss.1	⊢ 𝐴 ∈ V
Assertion	r1elss	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )

Proof

Step	Hyp	Ref	Expression
1		r1elss.1	⊢ 𝐴 ∈ V
2		r1elssi	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )
3	1	tz9.12	⊢ ( ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) )
4		dfss3	⊢ ( 𝐴 ⊆ ∪ ( 𝑅1 “ On ) ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ∪ ( 𝑅1 “ On ) )
5		r1fnon	⊢ 𝑅1 Fn On
6		fnfun	⊢ ( 𝑅1 Fn On → Fun 𝑅1 )
7		funiunfv	⊢ ( Fun 𝑅1 → ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = ∪ ( 𝑅1 “ On ) )
8	5 6 7	mp2b	⊢ ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = ∪ ( 𝑅1 “ On )
9	8	eleq2i	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) ↔ 𝑦 ∈ ∪ ( 𝑅1 “ On ) )
10		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) )
11	9 10	bitr3i	⊢ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) )
12	11	ralbii	⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ∪ ( 𝑅1 “ On ) ↔ ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) )
13	4 12	bitri	⊢ ( 𝐴 ⊆ ∪ ( 𝑅1 “ On ) ↔ ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) )
14	8	eleq2i	⊢ ( 𝐴 ∈ ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) ↔ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
15		eliun	⊢ ( 𝐴 ∈ ∪ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) )
16	14 15	bitr3i	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) )
17	3 13 16	3imtr4i	⊢ ( 𝐴 ⊆ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
18	2 17	impbii	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )