Theorem orbitclmpt

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

	Ref	Expression
Hypotheses	orbitclmpt.1	⊢ Ⅎ 𝑥 𝐵
	orbitclmpt.2	⊢ Ⅎ 𝑥 𝐷
	orbitclmpt.3	⊢ 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) “ ω )
	orbitclmpt.4	⊢ ( 𝑥 = 𝐵 → 𝐶 = 𝐷 )
Assertion	orbitclmpt	⊢ ( ( 𝐵 ∈ 𝑍 ∧ 𝐷 ∈ 𝑉 ) → 𝐷 ∈ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		orbitclmpt.1	⊢ Ⅎ 𝑥 𝐵
2		orbitclmpt.2	⊢ Ⅎ 𝑥 𝐷
3		orbitclmpt.3	⊢ 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) “ ω )
4		orbitclmpt.4	⊢ ( 𝑥 = 𝐵 → 𝐶 = 𝐷 )
5		elex	⊢ ( 𝐵 ∈ 𝑍 → 𝐵 ∈ V )
6		eqid	⊢ ( 𝑥 ∈ V ↦ 𝐶 ) = ( 𝑥 ∈ V ↦ 𝐶 )
7	1 2 4 6	fvmptf	⊢ ( ( 𝐵 ∈ V ∧ 𝐷 ∈ 𝑉 ) → ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ 𝐵 ) = 𝐷 )
8	5 7	sylan	⊢ ( ( 𝐵 ∈ 𝑍 ∧ 𝐷 ∈ 𝑉 ) → ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ 𝐵 ) = 𝐷 )
9		orbitcl	⊢ ( 𝐵 ∈ ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) “ ω ) → ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ 𝐵 ) ∈ ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) “ ω ) )
10	3	eleq2i	⊢ ( 𝐵 ∈ 𝑍 ↔ 𝐵 ∈ ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) “ ω ) )
11	3	eleq2i	⊢ ( ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ 𝐵 ) ∈ 𝑍 ↔ ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ 𝐵 ) ∈ ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) “ ω ) )
12	9 10 11	3imtr4i	⊢ ( 𝐵 ∈ 𝑍 → ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ 𝐵 ) ∈ 𝑍 )
13	12	adantr	⊢ ( ( 𝐵 ∈ 𝑍 ∧ 𝐷 ∈ 𝑉 ) → ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ 𝐵 ) ∈ 𝑍 )
14	8 13	eqeltrrd	⊢ ( ( 𝐵 ∈ 𝑍 ∧ 𝐷 ∈ 𝑉 ) → 𝐷 ∈ 𝑍 )