Metamath Proof Explorer

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 ⊢ A ∈ V
Assertion r1elss ⊢ A ∈ ⋃ R1 On ↔ A ⊆ ⋃ R1 On

Proof

Step Hyp Ref Expression
1 r1elss.1 ⊢ A ∈ V
2 r1elssi ⊢ A ∈ ⋃ R1 On → A ⊆ ⋃ R1 On
3 1 tz9.12 ⊢ ∀ y ∈ A ∃ x ∈ On y ∈ R1 ⁡ x → ∃ x ∈ On A ∈ R1 ⁡ x
4 dfss3 ⊢ A ⊆ ⋃ R1 On ↔ ∀ y ∈ A y ∈ ⋃ R1 On
5 r1fnon ⊢ R1 Fn On
6 fnfun ⊢ R1 Fn On → Fun ⁡ R1
7 funiunfv ⊢ Fun ⁡ R1 → ⋃ x ∈ On R1 ⁡ x = ⋃ R1 On
8 5 6 7 mp2b ⊢ ⋃ x ∈ On R1 ⁡ x = ⋃ R1 On
9 8 eleq2i ⊢ y ∈ ⋃ x ∈ On R1 ⁡ x ↔ y ∈ ⋃ R1 On
10 eliun ⊢ y ∈ ⋃ x ∈ On R1 ⁡ x ↔ ∃ x ∈ On y ∈ R1 ⁡ x
11 9 10 bitr3i ⊢ y ∈ ⋃ R1 On ↔ ∃ x ∈ On y ∈ R1 ⁡ x
12 11 ralbii ⊢ ∀ y ∈ A y ∈ ⋃ R1 On ↔ ∀ y ∈ A ∃ x ∈ On y ∈ R1 ⁡ x
13 4 12 bitri ⊢ A ⊆ ⋃ R1 On ↔ ∀ y ∈ A ∃ x ∈ On y ∈ R1 ⁡ x
14 8 eleq2i ⊢ A ∈ ⋃ x ∈ On R1 ⁡ x ↔ A ∈ ⋃ R1 On
15 eliun ⊢ A ∈ ⋃ x ∈ On R1 ⁡ x ↔ ∃ x ∈ On A ∈ R1 ⁡ x
16 14 15 bitr3i ⊢ A ∈ ⋃ R1 On ↔ ∃ x ∈ On A ∈ R1 ⁡ x
17 3 13 16 3imtr4i ⊢ A ⊆ ⋃ R1 On → A ∈ ⋃ R1 On
18 2 17 impbii ⊢ A ∈ ⋃ R1 On ↔ A ⊆ ⋃ R1 On