cantnfrescl

Description: A function is finitely supported from B to A iff the extended function is finitely supported from D to A . (Contributed by Mario Carneiro, 25-May-2015)

	Ref	Expression
Hypotheses	cantnfs.s	⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
	cantnfs.a	⊢ ( 𝜑 → 𝐴 ∈ On )
	cantnfs.b	⊢ ( 𝜑 → 𝐵 ∈ On )
	cantnfrescl.d	⊢ ( 𝜑 → 𝐷 ∈ On )
	cantnfrescl.b	⊢ ( 𝜑 → 𝐵 ⊆ 𝐷 )
	cantnfrescl.x	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐷 ∖ 𝐵 ) ) → 𝑋 = ∅ )
	cantnfrescl.a	⊢ ( 𝜑 → ∅ ∈ 𝐴 )
	cantnfrescl.t	⊢ 𝑇 = dom ( 𝐴 CNF 𝐷 )
Assertion	cantnfrescl	⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ∈ 𝑆 ↔ ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ∈ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
2		cantnfs.a	⊢ ( 𝜑 → 𝐴 ∈ On )
3		cantnfs.b	⊢ ( 𝜑 → 𝐵 ∈ On )
4		cantnfrescl.d	⊢ ( 𝜑 → 𝐷 ∈ On )
5		cantnfrescl.b	⊢ ( 𝜑 → 𝐵 ⊆ 𝐷 )
6		cantnfrescl.x	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐷 ∖ 𝐵 ) ) → 𝑋 = ∅ )
7		cantnfrescl.a	⊢ ( 𝜑 → ∅ ∈ 𝐴 )
8		cantnfrescl.t	⊢ 𝑇 = dom ( 𝐴 CNF 𝐷 )
9	7	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐷 ∖ 𝐵 ) ) → ∅ ∈ 𝐴 )
10	6 9	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐷 ∖ 𝐵 ) ) → 𝑋 ∈ 𝐴 )
11	10	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ( 𝐷 ∖ 𝐵 ) 𝑋 ∈ 𝐴 )
12	5 11	raldifeq	⊢ ( 𝜑 → ( ∀ 𝑛 ∈ 𝐵 𝑋 ∈ 𝐴 ↔ ∀ 𝑛 ∈ 𝐷 𝑋 ∈ 𝐴 ) )
13		eqid	⊢ ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) = ( 𝑛 ∈ 𝐵 ↦ 𝑋 )
14	13	fmpt	⊢ ( ∀ 𝑛 ∈ 𝐵 𝑋 ∈ 𝐴 ↔ ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) : 𝐵 ⟶ 𝐴 )
15		eqid	⊢ ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) = ( 𝑛 ∈ 𝐷 ↦ 𝑋 )
16	15	fmpt	⊢ ( ∀ 𝑛 ∈ 𝐷 𝑋 ∈ 𝐴 ↔ ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) : 𝐷 ⟶ 𝐴 )
17	12 14 16	3bitr3g	⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) : 𝐵 ⟶ 𝐴 ↔ ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) : 𝐷 ⟶ 𝐴 ) )
18	3	mptexd	⊢ ( 𝜑 → ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ∈ V )
19		funmpt	⊢ Fun ( 𝑛 ∈ 𝐵 ↦ 𝑋 )
20	19	a1i	⊢ ( 𝜑 → Fun ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) )
21	4	mptexd	⊢ ( 𝜑 → ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ∈ V )
22		funmpt	⊢ Fun ( 𝑛 ∈ 𝐷 ↦ 𝑋 )
23	21 22	jctir	⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ∈ V ∧ Fun ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ) )
24	18 20 23	jca31	⊢ ( 𝜑 → ( ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ∈ V ∧ Fun ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ) ∧ ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ∈ V ∧ Fun ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ) ) )
25	4 5 6	extmptsuppeq	⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) = ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) )
26		suppeqfsuppbi	⊢ ( ( ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ∈ V ∧ Fun ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ) ∧ ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ∈ V ∧ Fun ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ) ) → ( ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) = ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) → ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) finSupp ∅ ↔ ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) finSupp ∅ ) ) )
27	24 25 26	sylc	⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) finSupp ∅ ↔ ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) finSupp ∅ ) )
28	17 27	anbi12d	⊢ ( 𝜑 → ( ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) : 𝐵 ⟶ 𝐴 ∧ ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) finSupp ∅ ) ↔ ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) : 𝐷 ⟶ 𝐴 ∧ ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) finSupp ∅ ) ) )
29	1 2 3	cantnfs	⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ∈ 𝑆 ↔ ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) : 𝐵 ⟶ 𝐴 ∧ ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) finSupp ∅ ) ) )
30	8 2 4	cantnfs	⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ∈ 𝑇 ↔ ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) : 𝐷 ⟶ 𝐴 ∧ ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) finSupp ∅ ) ) )
31	28 29 30	3bitr4d	⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ∈ 𝑆 ↔ ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ∈ 𝑇 ) )

Metamath Proof Explorer

Theorem cantnfrescl

Proof