Theorem cantnfrescl 9673

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 2827	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐷 ∖ 𝐵)) → 𝑋 ∈ 𝐴)
6	5	ralrimiva 3140	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ (𝐷 ∖ 𝐵)𝑋 ∈ 𝐴)
7	1, 6	raldifeq 4488	. . . 4 ⊢ (𝜑 → (∀𝑛 ∈ 𝐵 𝑋 ∈ 𝐴 ↔ ∀𝑛 ∈ 𝐷 𝑋 ∈ 𝐴))
8		eqid 2726	. . . . 5 ⊢ (𝑛 ∈ 𝐵 ↦ 𝑋) = (𝑛 ∈ 𝐵 ↦ 𝑋)
9	8	fmpt 7105	. . . 4 ⊢ (∀𝑛 ∈ 𝐵 𝑋 ∈ 𝐴 ↔ (𝑛 ∈ 𝐵 ↦ 𝑋):𝐵⟶𝐴)
10		eqid 2726	. . . . 5 ⊢ (𝑛 ∈ 𝐷 ↦ 𝑋) = (𝑛 ∈ 𝐷 ↦ 𝑋)
11	10	fmpt 7105	. . . 4 ⊢ (∀𝑛 ∈ 𝐷 𝑋 ∈ 𝐴 ↔ (𝑛 ∈ 𝐷 ↦ 𝑋):𝐷⟶𝐴)
12	7, 9, 11	3bitr3g 313	. . 3 ⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋):𝐵⟶𝐴 ↔ (𝑛 ∈ 𝐷 ↦ 𝑋):𝐷⟶𝐴))
13		cantnfs.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ On)
14	13	mptexd 7221	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ 𝐵 ↦ 𝑋) ∈ V)
15		funmpt 6580	. . . . . 6 ⊢ Fun (𝑛 ∈ 𝐵 ↦ 𝑋)
16	15	a1i 11	. . . . 5 ⊢ (𝜑 → Fun (𝑛 ∈ 𝐵 ↦ 𝑋))
17		cantnfrescl.d	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ On)
18	17	mptexd 7221	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ 𝐷 ↦ 𝑋) ∈ V)
19		funmpt 6580	. . . . . 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 8173	. . . 4 ⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅) = ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))
23		suppeqfsuppbi 9379	. . . 4 ⊢ ((((𝑛 ∈ 𝐵 ↦ 𝑋) ∈ V ∧ Fun (𝑛 ∈ 𝐵 ↦ 𝑋)) ∧ ((𝑛 ∈ 𝐷 ↦ 𝑋) ∈ V ∧ Fun (𝑛 ∈ 𝐷 ↦ 𝑋))) → (((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅) = ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅) → ((𝑛 ∈ 𝐵 ↦ 𝑋) finSupp ∅ ↔ (𝑛 ∈ 𝐷 ↦ 𝑋) finSupp ∅)))
24	21, 22, 23	sylc 65	. . 3 ⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) finSupp ∅ ↔ (𝑛 ∈ 𝐷 ↦ 𝑋) finSupp ∅))
25	12, 24	anbi12d 630	. 2 ⊢ (𝜑 → (((𝑛 ∈ 𝐵 ↦ 𝑋):𝐵⟶𝐴 ∧ (𝑛 ∈ 𝐵 ↦ 𝑋) finSupp ∅) ↔ ((𝑛 ∈ 𝐷 ↦ 𝑋):𝐷⟶𝐴 ∧ (𝑛 ∈ 𝐷 ↦ 𝑋) finSupp ∅)))
26		cantnfs.s	. . 3 ⊢ 𝑆 = dom (𝐴 CNF 𝐵)
27		cantnfs.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ On)
28	26, 27, 13	cantnfs 9663	. 2 ⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) ∈ 𝑆 ↔ ((𝑛 ∈ 𝐵 ↦ 𝑋):𝐵⟶𝐴 ∧ (𝑛 ∈ 𝐵 ↦ 𝑋) finSupp ∅)))
29		cantnfrescl.t	. . 3 ⊢ 𝑇 = dom (𝐴 CNF 𝐷)
30	29, 27, 17	cantnfs 9663	. 2 ⊢ (𝜑 → ((𝑛 ∈ 𝐷 ↦ 𝑋) ∈ 𝑇 ↔ ((𝑛 ∈ 𝐷 ↦ 𝑋):𝐷⟶𝐴 ∧ (𝑛 ∈ 𝐷 ↦ 𝑋) finSupp ∅)))
31	25, 28, 30	3bitr4d 311	1 ⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) ∈ 𝑆 ↔ (𝑛 ∈ 𝐷 ↦ 𝑋) ∈ 𝑇))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098  ∀wral 3055  Vcvv 3468   ∖ cdif 3940   ⊆ wss 3943  ∅c0 4317   class class class wbr 5141   ↦ cmpt 5224  dom cdm 5669  Oncon0 6358  Fun wfun 6531  ⟶wf 6533  (class class class)co 7405   supp csupp 8146   finSupp cfsupp 9363   CNF ccnf 9658

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7408  df-oprab 7409  df-mpo 7410  df-supp 8147  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-seqom 8449  df-map 8824  df-fsupp 9364  df-cnf 9659

This theorem is referenced by:  cantnfres  9674