This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )