Metamath Proof Explorer

Theorem orbitclmpt

Description: Version of orbitcl using maps-to notation. (Contributed by Eric Schmidt, 6-Nov-2025)

Ref Expression
Hypotheses orbitclmpt.1 ⊢ Ⅎ _ x B
orbitclmpt.2 ⊢ Ⅎ _ x D
orbitclmpt.3 ⊢ Z = rec ⁡ x ∈ V ⟼ C A ω
orbitclmpt.4 ⊢ x = B → C = D
Assertion orbitclmpt ⊢ B ∈ Z ∧ D ∈ V → D ∈ Z

Proof

Step Hyp Ref Expression
1 orbitclmpt.1 ⊢ Ⅎ _ x B
2 orbitclmpt.2 ⊢ Ⅎ _ x D
3 orbitclmpt.3 ⊢ Z = rec ⁡ x ∈ V ⟼ C A ω
4 orbitclmpt.4 ⊢ x = B → C = D
5 elex ⊢ B ∈ Z → B ∈ V
6 eqid ⊢ x ∈ V ⟼ C = x ∈ V ⟼ C
7 1 2 4 6 fvmptf ⊢ B ∈ V ∧ D ∈ V → x ∈ V ⟼ C ⁡ B = D
8 5 7 sylan ⊢ B ∈ Z ∧ D ∈ V → x ∈ V ⟼ C ⁡ B = D
9 orbitcl ⊢ B ∈ rec ⁡ x ∈ V ⟼ C A ω → x ∈ V ⟼ C ⁡ B ∈ rec ⁡ x ∈ V ⟼ C A ω
10 3 eleq2i ⊢ B ∈ Z ↔ B ∈ rec ⁡ x ∈ V ⟼ C A ω
11 3 eleq2i ⊢ x ∈ V ⟼ C ⁡ B ∈ Z ↔ x ∈ V ⟼ C ⁡ B ∈ rec ⁡ x ∈ V ⟼ C A ω
12 9 10 11 3imtr4i ⊢ B ∈ Z → x ∈ V ⟼ C ⁡ B ∈ Z
13 12 adantr ⊢ B ∈ Z ∧ D ∈ V → x ∈ V ⟼ C ⁡ B ∈ Z
14 8 13 eqeltrrd ⊢ B ∈ Z ∧ D ∈ V → D ∈ Z