MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cantnfp1lem1 Structured version   Visualization version   GIF version

Theorem cantnfp1lem1 8818
Description: Lemma for cantnfp1 8821. (Contributed by Mario Carneiro, 20-Jun-2015.) (Revised by AV, 30-Jun-2019.)
Hypotheses
Ref Expression
cantnfs.s 𝑆 = dom (𝐴 CNF 𝐵)
cantnfs.a (𝜑𝐴 ∈ On)
cantnfs.b (𝜑𝐵 ∈ On)
cantnfp1.g (𝜑𝐺𝑆)
cantnfp1.x (𝜑𝑋𝐵)
cantnfp1.y (𝜑𝑌𝐴)
cantnfp1.s (𝜑 → (𝐺 supp ∅) ⊆ 𝑋)
cantnfp1.f 𝐹 = (𝑡𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)))
Assertion
Ref Expression
cantnfp1lem1 (𝜑𝐹𝑆)
Distinct variable groups:   𝑡,𝐵   𝑡,𝐴   𝑡,𝑆   𝑡,𝐺   𝜑,𝑡   𝑡,𝑌   𝑡,𝑋
Allowed substitution hint:   𝐹(𝑡)

Proof of Theorem cantnfp1lem1
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 cantnfp1.y . . . . 5 (𝜑𝑌𝐴)
21adantr 468 . . . 4 ((𝜑𝑡𝐵) → 𝑌𝐴)
3 cantnfp1.g . . . . . . 7 (𝜑𝐺𝑆)
4 cantnfs.s . . . . . . . 8 𝑆 = dom (𝐴 CNF 𝐵)
5 cantnfs.a . . . . . . . 8 (𝜑𝐴 ∈ On)
6 cantnfs.b . . . . . . . 8 (𝜑𝐵 ∈ On)
74, 5, 6cantnfs 8806 . . . . . . 7 (𝜑 → (𝐺𝑆 ↔ (𝐺:𝐵𝐴𝐺 finSupp ∅)))
83, 7mpbid 223 . . . . . 6 (𝜑 → (𝐺:𝐵𝐴𝐺 finSupp ∅))
98simpld 484 . . . . 5 (𝜑𝐺:𝐵𝐴)
109ffvelrnda 6577 . . . 4 ((𝜑𝑡𝐵) → (𝐺𝑡) ∈ 𝐴)
112, 10ifcld 4324 . . 3 ((𝜑𝑡𝐵) → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) ∈ 𝐴)
12 cantnfp1.f . . 3 𝐹 = (𝑡𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)))
1311, 12fmptd 6602 . 2 (𝜑𝐹:𝐵𝐴)
148simprd 485 . . . . . 6 (𝜑𝐺 finSupp ∅)
1514fsuppimpd 8517 . . . . 5 (𝜑 → (𝐺 supp ∅) ∈ Fin)
16 snfi 8273 . . . . 5 {𝑋} ∈ Fin
17 unfi 8462 . . . . 5 (((𝐺 supp ∅) ∈ Fin ∧ {𝑋} ∈ Fin) → ((𝐺 supp ∅) ∪ {𝑋}) ∈ Fin)
1815, 16, 17sylancl 576 . . . 4 (𝜑 → ((𝐺 supp ∅) ∪ {𝑋}) ∈ Fin)
19 eldifi 3931 . . . . . . . 8 (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → 𝑘𝐵)
2019adantl 469 . . . . . . 7 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → 𝑘𝐵)
211adantr 468 . . . . . . . 8 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → 𝑌𝐴)
22 fvex 6417 . . . . . . . 8 (𝐺𝑘) ∈ V
23 ifexg 4326 . . . . . . . 8 ((𝑌𝐴 ∧ (𝐺𝑘) ∈ V) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V)
2421, 22, 23sylancl 576 . . . . . . 7 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V)
25 eqeq1 2810 . . . . . . . . 9 (𝑡 = 𝑘 → (𝑡 = 𝑋𝑘 = 𝑋))
26 fveq2 6404 . . . . . . . . 9 (𝑡 = 𝑘 → (𝐺𝑡) = (𝐺𝑘))
2725, 26ifbieq2d 4304 . . . . . . . 8 (𝑡 = 𝑘 → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
2827, 12fvmptg 6497 . . . . . . 7 ((𝑘𝐵 ∧ if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V) → (𝐹𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
2920, 24, 28syl2anc 575 . . . . . 6 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐹𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
30 eldifn 3932 . . . . . . . . 9 (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → ¬ 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
3130adantl 469 . . . . . . . 8 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → ¬ 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
32 velsn 4386 . . . . . . . . 9 (𝑘 ∈ {𝑋} ↔ 𝑘 = 𝑋)
33 elun2 3980 . . . . . . . . 9 (𝑘 ∈ {𝑋} → 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
3432, 33sylbir 226 . . . . . . . 8 (𝑘 = 𝑋𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
3531, 34nsyl 137 . . . . . . 7 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → ¬ 𝑘 = 𝑋)
3635iffalsed 4290 . . . . . 6 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = (𝐺𝑘))
37 ssun1 3975 . . . . . . . . 9 (𝐺 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋})
38 sscon 3943 . . . . . . . . 9 ((𝐺 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋}) → (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) ⊆ (𝐵 ∖ (𝐺 supp ∅)))
3937, 38ax-mp 5 . . . . . . . 8 (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) ⊆ (𝐵 ∖ (𝐺 supp ∅))
4039sseli 3794 . . . . . . 7 (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → 𝑘 ∈ (𝐵 ∖ (𝐺 supp ∅)))
41 eqid 2806 . . . . . . . . 9 (𝐺 supp ∅) = (𝐺 supp ∅)
42 eqimss2 3855 . . . . . . . . 9 ((𝐺 supp ∅) = (𝐺 supp ∅) → (𝐺 supp ∅) ⊆ (𝐺 supp ∅))
4341, 42mp1i 13 . . . . . . . 8 (𝜑 → (𝐺 supp ∅) ⊆ (𝐺 supp ∅))
44 0ex 4984 . . . . . . . . 9 ∅ ∈ V
4544a1i 11 . . . . . . . 8 (𝜑 → ∅ ∈ V)
469, 43, 6, 45suppssr 7557 . . . . . . 7 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐺 supp ∅))) → (𝐺𝑘) = ∅)
4740, 46sylan2 582 . . . . . 6 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐺𝑘) = ∅)
4829, 36, 473eqtrd 2844 . . . . 5 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐹𝑘) = ∅)
4913, 48suppss 7556 . . . 4 (𝜑 → (𝐹 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋}))
50 ssfi 8415 . . . 4 ((((𝐺 supp ∅) ∪ {𝑋}) ∈ Fin ∧ (𝐹 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋})) → (𝐹 supp ∅) ∈ Fin)
5118, 49, 50syl2anc 575 . . 3 (𝜑 → (𝐹 supp ∅) ∈ Fin)
5212funmpt2 6136 . . . . 5 Fun 𝐹
5352a1i 11 . . . 4 (𝜑 → Fun 𝐹)
54 mptexg 6705 . . . . . 6 (𝐵 ∈ On → (𝑡𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺𝑡))) ∈ V)
5512, 54syl5eqel 2889 . . . . 5 (𝐵 ∈ On → 𝐹 ∈ V)
566, 55syl 17 . . . 4 (𝜑𝐹 ∈ V)
57 funisfsupp 8515 . . . 4 ((Fun 𝐹𝐹 ∈ V ∧ ∅ ∈ V) → (𝐹 finSupp ∅ ↔ (𝐹 supp ∅) ∈ Fin))
5853, 56, 45, 57syl3anc 1483 . . 3 (𝜑 → (𝐹 finSupp ∅ ↔ (𝐹 supp ∅) ∈ Fin))
5951, 58mpbird 248 . 2 (𝜑𝐹 finSupp ∅)
604, 5, 6cantnfs 8806 . 2 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐵𝐴𝐹 finSupp ∅)))
6113, 59, 60mpbir2and 695 1 (𝜑𝐹𝑆)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1637  wcel 2156  Vcvv 3391  cdif 3766  cun 3767  wss 3769  c0 4116  ifcif 4279  {csn 4370   class class class wbr 4844  cmpt 4923  dom cdm 5311  Oncon0 5936  Fun wfun 6091  wf 6093  cfv 6097  (class class class)co 6870   supp csupp 7525  Fincfn 8188   finSupp cfsupp 8510   CNF ccnf 8801
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-om 7292  df-supp 7526  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-seqom 7775  df-1o 7792  df-oadd 7796  df-er 7975  df-map 8090  df-en 8189  df-fin 8192  df-fsupp 8511  df-cnf 8802
This theorem is referenced by:  cantnfp1lem2  8819  cantnfp1lem3  8820  cantnfp1  8821
  Copyright terms: Public domain W3C validator