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 ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ∈ ( 𝑅1 ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 r1elwf ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
2 rankelb ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝐶 ∈ 𝐴 → ( rank ‘ 𝐶 ) ∈ ( rank ‘ 𝐴 ) ) )
3 1 2 syl ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( 𝐶 ∈ 𝐴 → ( rank ‘ 𝐶 ) ∈ ( rank ‘ 𝐴 ) ) )
4 3 imp ⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → ( rank ‘ 𝐶 ) ∈ ( rank ‘ 𝐴 ) )
5 rankr1ai ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( rank ‘ 𝐴 ) ∈ 𝐵 )
6 elfvdm ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐵 ∈ dom 𝑅1 )
7 r1fnon ⊢ 𝑅1 Fn On
8 7 fndmi ⊢ dom 𝑅1 = On
9 6 8 eleqtrdi ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝐵 ∈ On )
10 ontr1 ⊢ ( 𝐵 ∈ On → ( ( ( rank ‘ 𝐶 ) ∈ ( rank ‘ 𝐴 ) ∧ ( rank ‘ 𝐴 ) ∈ 𝐵 ) → ( rank ‘ 𝐶 ) ∈ 𝐵 ) )
11 9 10 syl ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( ( ( rank ‘ 𝐶 ) ∈ ( rank ‘ 𝐴 ) ∧ ( rank ‘ 𝐴 ) ∈ 𝐵 ) → ( rank ‘ 𝐶 ) ∈ 𝐵 ) )
12 5 11 mpan2d ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( ( rank ‘ 𝐶 ) ∈ ( rank ‘ 𝐴 ) → ( rank ‘ 𝐶 ) ∈ 𝐵 ) )
13 12 adantr ⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → ( ( rank ‘ 𝐶 ) ∈ ( rank ‘ 𝐴 ) → ( rank ‘ 𝐶 ) ∈ 𝐵 ) )
14 4 13 mpd ⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → ( rank ‘ 𝐶 ) ∈ 𝐵 )
15 elwf ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ∈ ∪ ( 𝑅1 “ On ) )
16 1 15 sylan ⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ∈ ∪ ( 𝑅1 “ On ) )
17 rankr1ag ⊢ ( ( 𝐶 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐶 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐶 ) ∈ 𝐵 ) )
18 6 17 sylan2 ⊢ ( ( 𝐶 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ) → ( 𝐶 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐶 ) ∈ 𝐵 ) )
19 18 ancoms ⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝐶 ∈ ∪ ( 𝑅1 “ On ) ) → ( 𝐶 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐶 ) ∈ 𝐵 ) )
20 16 19 syldan ⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → ( 𝐶 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐶 ) ∈ 𝐵 ) )
21 14 20 mpbird ⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ∈ ( 𝑅1 ‘ 𝐵 ) )