This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ∈ 𝑆 ↔ ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ∈ 𝑇 ) )