Metamath Proof Explorer

Theorem r1elcl

Description: Each set of the cumulative hierarchy is closed under membership. (Contributed by BTernaryTau, 30-Dec-2025)

Ref Expression
Assertion r1elcl ⊢ A ∈ R1 ⁡ B ∧ C ∈ A → C ∈ R1 ⁡ B

Proof

Step Hyp Ref Expression
1 r1elwf ⊢ A ∈ R1 ⁡ B → A ∈ ⋃ R1 On
2 rankelb ⊢ A ∈ ⋃ R1 On → C ∈ A → rank ⁡ C ∈ rank ⁡ A
3 1 2 syl ⊢ A ∈ R1 ⁡ B → C ∈ A → rank ⁡ C ∈ rank ⁡ A
4 3 imp ⊢ A ∈ R1 ⁡ B ∧ C ∈ A → rank ⁡ C ∈ rank ⁡ A
5 rankr1ai ⊢ A ∈ R1 ⁡ B → rank ⁡ A ∈ B
6 elfvdm ⊢ A ∈ R1 ⁡ B → B ∈ dom ⁡ R1
7 r1fnon ⊢ R1 Fn On
8 7 fndmi ⊢ dom ⁡ R1 = On
9 6 8 eleqtrdi ⊢ A ∈ R1 ⁡ B → B ∈ On
10 ontr1 ⊢ B ∈ On → rank ⁡ C ∈ rank ⁡ A ∧ rank ⁡ A ∈ B → rank ⁡ C ∈ B
11 9 10 syl ⊢ A ∈ R1 ⁡ B → rank ⁡ C ∈ rank ⁡ A ∧ rank ⁡ A ∈ B → rank ⁡ C ∈ B
12 5 11 mpan2d ⊢ A ∈ R1 ⁡ B → rank ⁡ C ∈ rank ⁡ A → rank ⁡ C ∈ B
13 12 adantr ⊢ A ∈ R1 ⁡ B ∧ C ∈ A → rank ⁡ C ∈ rank ⁡ A → rank ⁡ C ∈ B
14 4 13 mpd ⊢ A ∈ R1 ⁡ B ∧ C ∈ A → rank ⁡ C ∈ B
15 elwf ⊢ A ∈ ⋃ R1 On ∧ C ∈ A → C ∈ ⋃ R1 On
16 1 15 sylan ⊢ A ∈ R1 ⁡ B ∧ C ∈ A → C ∈ ⋃ R1 On
17 rankr1ag ⊢ C ∈ ⋃ R1 On ∧ B ∈ dom ⁡ R1 → C ∈ R1 ⁡ B ↔ rank ⁡ C ∈ B
18 6 17 sylan2 ⊢ C ∈ ⋃ R1 On ∧ A ∈ R1 ⁡ B → C ∈ R1 ⁡ B ↔ rank ⁡ C ∈ B
19 18 ancoms ⊢ A ∈ R1 ⁡ B ∧ C ∈ ⋃ R1 On → C ∈ R1 ⁡ B ↔ rank ⁡ C ∈ B
20 16 19 syldan ⊢ A ∈ R1 ⁡ B ∧ C ∈ A → C ∈ R1 ⁡ B ↔ rank ⁡ C ∈ B
21 14 20 mpbird ⊢ A ∈ R1 ⁡ B ∧ C ∈ A → C ∈ R1 ⁡ B