Theorem cantnfrescl 9697

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 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐷 ∖ 𝐵)) → ∅ ∈ 𝐴)
5	2, 4	eqeltrd 2833	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐷 ∖ 𝐵)) → 𝑋 ∈ 𝐴)
6	5	ralrimiva 3133	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ (𝐷 ∖ 𝐵)𝑋 ∈ 𝐴)
7	1, 6	raldifeq 4474	. . . 4 ⊢ (𝜑 → (∀𝑛 ∈ 𝐵 𝑋 ∈ 𝐴 ↔ ∀𝑛 ∈ 𝐷 𝑋 ∈ 𝐴))
8		eqid 2734	. . . . 5 ⊢ (𝑛 ∈ 𝐵 ↦ 𝑋) = (𝑛 ∈ 𝐵 ↦ 𝑋)
9	8	fmpt 7109	. . . 4 ⊢ (∀𝑛 ∈ 𝐵 𝑋 ∈ 𝐴 ↔ (𝑛 ∈ 𝐵 ↦ 𝑋):𝐵⟶𝐴)
10		eqid 2734	. . . . 5 ⊢ (𝑛 ∈ 𝐷 ↦ 𝑋) = (𝑛 ∈ 𝐷 ↦ 𝑋)
11	10	fmpt 7109	. . . 4 ⊢ (∀𝑛 ∈ 𝐷 𝑋 ∈ 𝐴 ↔ (𝑛 ∈ 𝐷 ↦ 𝑋):𝐷⟶𝐴)
12	7, 9, 11	3bitr3g 313	. . 3 ⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋):𝐵⟶𝐴 ↔ (𝑛 ∈ 𝐷 ↦ 𝑋):𝐷⟶𝐴))
13		cantnfs.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ On)
14	13	mptexd 7225	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ 𝐵 ↦ 𝑋) ∈ V)
15		funmpt 6583	. . . . . 6 ⊢ Fun (𝑛 ∈ 𝐵 ↦ 𝑋)
16	15	a1i 11	. . . . 5 ⊢ (𝜑 → Fun (𝑛 ∈ 𝐵 ↦ 𝑋))
17		cantnfrescl.d	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ On)
18	17	mptexd 7225	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ 𝐷 ↦ 𝑋) ∈ V)
19		funmpt 6583	. . . . . 6 ⊢ Fun (𝑛 ∈ 𝐷 ↦ 𝑋)
20	18, 19	jctir 520	. . . . 5 ⊢ (𝜑 → ((𝑛 ∈ 𝐷 ↦ 𝑋) ∈ V ∧ Fun (𝑛 ∈ 𝐷 ↦ 𝑋)))
21	14, 16, 20	jca31 514	. . . 4 ⊢ (𝜑 → (((𝑛 ∈ 𝐵 ↦ 𝑋) ∈ V ∧ Fun (𝑛 ∈ 𝐵 ↦ 𝑋)) ∧ ((𝑛 ∈ 𝐷 ↦ 𝑋) ∈ V ∧ Fun (𝑛 ∈ 𝐷 ↦ 𝑋))))
22	17, 1, 2	extmptsuppeq 8194	. . . 4 ⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅) = ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))
23		suppeqfsuppbi 9400	. . . 4 ⊢ ((((𝑛 ∈ 𝐵 ↦ 𝑋) ∈ V ∧ Fun (𝑛 ∈ 𝐵 ↦ 𝑋)) ∧ ((𝑛 ∈ 𝐷 ↦ 𝑋) ∈ V ∧ Fun (𝑛 ∈ 𝐷 ↦ 𝑋))) → (((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅) = ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅) → ((𝑛 ∈ 𝐵 ↦ 𝑋) finSupp ∅ ↔ (𝑛 ∈ 𝐷 ↦ 𝑋) finSupp ∅)))
24	21, 22, 23	sylc 65	. . 3 ⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) finSupp ∅ ↔ (𝑛 ∈ 𝐷 ↦ 𝑋) finSupp ∅))
25	12, 24	anbi12d 632	. 2 ⊢ (𝜑 → (((𝑛 ∈ 𝐵 ↦ 𝑋):𝐵⟶𝐴 ∧ (𝑛 ∈ 𝐵 ↦ 𝑋) finSupp ∅) ↔ ((𝑛 ∈ 𝐷 ↦ 𝑋):𝐷⟶𝐴 ∧ (𝑛 ∈ 𝐷 ↦ 𝑋) finSupp ∅)))
26		cantnfs.s	. . 3 ⊢ 𝑆 = dom (𝐴 CNF 𝐵)
27		cantnfs.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ On)
28	26, 27, 13	cantnfs 9687	. 2 ⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) ∈ 𝑆 ↔ ((𝑛 ∈ 𝐵 ↦ 𝑋):𝐵⟶𝐴 ∧ (𝑛 ∈ 𝐵 ↦ 𝑋) finSupp ∅)))
29		cantnfrescl.t	. . 3 ⊢ 𝑇 = dom (𝐴 CNF 𝐷)
30	29, 27, 17	cantnfs 9687	. 2 ⊢ (𝜑 → ((𝑛 ∈ 𝐷 ↦ 𝑋) ∈ 𝑇 ↔ ((𝑛 ∈ 𝐷 ↦ 𝑋):𝐷⟶𝐴 ∧ (𝑛 ∈ 𝐷 ↦ 𝑋) finSupp ∅)))
31	25, 28, 30	3bitr4d 311	1 ⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) ∈ 𝑆 ↔ (𝑛 ∈ 𝐷 ↦ 𝑋) ∈ 𝑇))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ∀wral 3050  Vcvv 3463   ∖ cdif 3928   ⊆ wss 3931  ∅c0 4313   class class class wbr 5123   ↦ cmpt 5205  dom cdm 5665  Oncon0 6363  Fun wfun 6534  ⟶wf 6536  (class class class)co 7412   supp csupp 8166   finSupp cfsupp 9382   CNF ccnf 9682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5259  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7736

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-pred 6301  df-iota 6493  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7415  df-oprab 7416  df-mpo 7417  df-supp 8167  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-seqom 8469  df-map 8849  df-fsupp 9383  df-cnf 9683

This theorem is referenced by:  cantnfres  9698