Theorem cantnfrescl 9123

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

Hypotheses

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

Assertion

Ref	Expression
cantnfrescl	⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) ∈ 𝑆 ↔ (𝑛 ∈ 𝐷 ↦ 𝑋) ∈ 𝑇))

Distinct variable groups:   𝐵,𝑛   𝐷,𝑛   𝐴,𝑛   𝜑,𝑛

Allowed substitution hints:   𝑆(𝑛)   𝑇(𝑛)   𝑋(𝑛)

Proof of Theorem cantnfrescl

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  Vcvv 3441   ∖ cdif 3878   ⊆ wss 3881  ∅c0 4243   class class class wbr 5030   ↦ cmpt 5110  dom cdm 5519  Oncon0 6159  Fun wfun 6318  ⟶wf 6320  (class class class)co 7135   supp csupp 7813   finSupp cfsupp 8817   CNF ccnf 9108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-oprab 7139  df-mpo 7140  df-supp 7814  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-seqom 8067  df-map 8391  df-fsupp 8818  df-cnf 9109

This theorem is referenced by:  cantnfres  9124