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

Theorem infxpenc2lem2 8788
Description: Lemma for infxpenc2 8790. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 7-Jul-2019.)
Hypotheses
Ref Expression
infxpenc2.1 (𝜑𝐴 ∈ On)
infxpenc2.2 (𝜑 → ∀𝑏𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1𝑜)(𝑛𝑏):𝑏1-1-onto→(ω ↑𝑜 𝑤)))
infxpenc2.3 𝑊 = ((𝑥 ∈ (On ∖ 1𝑜) ↦ (ω ↑𝑜 𝑥))‘ran (𝑛𝑏))
infxpenc2.4 (𝜑𝐹:(ω ↑𝑜 2𝑜)–1-1-onto→ω)
infxpenc2.5 (𝜑 → (𝐹‘∅) = ∅)
infxpenc2.k 𝐾 = (𝑦 ∈ {𝑥 ∈ ((ω ↑𝑜 2𝑜) ↑𝑚 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦( I ↾ 𝑊))))
infxpenc2.h 𝐻 = (((ω CNF 𝑊) ∘ 𝐾) ∘ ((ω ↑𝑜 2𝑜) CNF 𝑊))
infxpenc2.l 𝐿 = (𝑦 ∈ {𝑥 ∈ (ω ↑𝑚 (𝑊 ·𝑜 2𝑜)) ∣ 𝑥 finSupp ∅} ↦ (( I ↾ ω) ∘ (𝑦(𝑌𝑋))))
infxpenc2.x 𝑋 = (𝑧 ∈ 2𝑜, 𝑤𝑊 ↦ ((𝑊 ·𝑜 𝑧) +𝑜 𝑤))
infxpenc2.y 𝑌 = (𝑧 ∈ 2𝑜, 𝑤𝑊 ↦ ((2𝑜 ·𝑜 𝑤) +𝑜 𝑧))
infxpenc2.j 𝐽 = (((ω CNF (2𝑜 ·𝑜 𝑊)) ∘ 𝐿) ∘ (ω CNF (𝑊 ·𝑜 2𝑜)))
infxpenc2.z 𝑍 = (𝑥 ∈ (ω ↑𝑜 𝑊), 𝑦 ∈ (ω ↑𝑜 𝑊) ↦ (((ω ↑𝑜 𝑊) ·𝑜 𝑥) +𝑜 𝑦))
infxpenc2.t 𝑇 = (𝑥𝑏, 𝑦𝑏 ↦ ⟨((𝑛𝑏)‘𝑥), ((𝑛𝑏)‘𝑦)⟩)
infxpenc2.g 𝐺 = ((𝑛𝑏) ∘ (((𝐻𝐽) ∘ 𝑍) ∘ 𝑇))
Assertion
Ref Expression
infxpenc2lem2 (𝜑 → ∃𝑔𝑏𝐴 (ω ⊆ 𝑏 → (𝑔𝑏):(𝑏 × 𝑏)–1-1-onto𝑏))
Distinct variable groups:   𝑔,𝑏,𝑛,𝑤,𝑥,𝑦,𝐴   𝜑,𝑏,𝑤,𝑥,𝑦   𝑧,𝑔,𝑊,𝑤,𝑥,𝑦   𝑔,𝐹,𝑥,𝑦   𝑔,𝐺   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦
Allowed substitution hints:   𝜑(𝑧,𝑔,𝑛)   𝐴(𝑧)   𝑇(𝑥,𝑦,𝑧,𝑤,𝑔,𝑛,𝑏)   𝐹(𝑧,𝑤,𝑛,𝑏)   𝐺(𝑥,𝑦,𝑧,𝑤,𝑛,𝑏)   𝐻(𝑥,𝑦,𝑧,𝑤,𝑔,𝑛,𝑏)   𝐽(𝑥,𝑦,𝑧,𝑤,𝑔,𝑛,𝑏)   𝐾(𝑥,𝑦,𝑧,𝑤,𝑔,𝑛,𝑏)   𝐿(𝑥,𝑦,𝑧,𝑤,𝑔,𝑛,𝑏)   𝑊(𝑛,𝑏)   𝑋(𝑧,𝑤,𝑔,𝑛,𝑏)   𝑌(𝑧,𝑤,𝑔,𝑛,𝑏)   𝑍(𝑥,𝑦,𝑧,𝑤,𝑔,𝑛,𝑏)

Proof of Theorem infxpenc2lem2
StepHypRef Expression
1 infxpenc2.1 . . 3 (𝜑𝐴 ∈ On)
2 mptexg 6439 . . 3 (𝐴 ∈ On → (𝑏𝐴𝐺) ∈ V)
31, 2syl 17 . 2 (𝜑 → (𝑏𝐴𝐺) ∈ V)
41adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → 𝐴 ∈ On)
5 simprl 793 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → 𝑏𝐴)
6 onelon 5710 . . . . . . 7 ((𝐴 ∈ On ∧ 𝑏𝐴) → 𝑏 ∈ On)
74, 5, 6syl2anc 692 . . . . . 6 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → 𝑏 ∈ On)
8 simprr 795 . . . . . 6 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → ω ⊆ 𝑏)
9 infxpenc2.2 . . . . . . . 8 (𝜑 → ∀𝑏𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1𝑜)(𝑛𝑏):𝑏1-1-onto→(ω ↑𝑜 𝑤)))
10 infxpenc2.3 . . . . . . . 8 𝑊 = ((𝑥 ∈ (On ∖ 1𝑜) ↦ (ω ↑𝑜 𝑥))‘ran (𝑛𝑏))
111, 9, 10infxpenc2lem1 8787 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → (𝑊 ∈ (On ∖ 1𝑜) ∧ (𝑛𝑏):𝑏1-1-onto→(ω ↑𝑜 𝑊)))
1211simpld 475 . . . . . 6 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → 𝑊 ∈ (On ∖ 1𝑜))
13 infxpenc2.4 . . . . . . 7 (𝜑𝐹:(ω ↑𝑜 2𝑜)–1-1-onto→ω)
1413adantr 481 . . . . . 6 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → 𝐹:(ω ↑𝑜 2𝑜)–1-1-onto→ω)
15 infxpenc2.5 . . . . . . 7 (𝜑 → (𝐹‘∅) = ∅)
1615adantr 481 . . . . . 6 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → (𝐹‘∅) = ∅)
1711simprd 479 . . . . . 6 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → (𝑛𝑏):𝑏1-1-onto→(ω ↑𝑜 𝑊))
18 infxpenc2.k . . . . . 6 𝐾 = (𝑦 ∈ {𝑥 ∈ ((ω ↑𝑜 2𝑜) ↑𝑚 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦( I ↾ 𝑊))))
19 infxpenc2.h . . . . . 6 𝐻 = (((ω CNF 𝑊) ∘ 𝐾) ∘ ((ω ↑𝑜 2𝑜) CNF 𝑊))
20 infxpenc2.l . . . . . 6 𝐿 = (𝑦 ∈ {𝑥 ∈ (ω ↑𝑚 (𝑊 ·𝑜 2𝑜)) ∣ 𝑥 finSupp ∅} ↦ (( I ↾ ω) ∘ (𝑦(𝑌𝑋))))
21 infxpenc2.x . . . . . 6 𝑋 = (𝑧 ∈ 2𝑜, 𝑤𝑊 ↦ ((𝑊 ·𝑜 𝑧) +𝑜 𝑤))
22 infxpenc2.y . . . . . 6 𝑌 = (𝑧 ∈ 2𝑜, 𝑤𝑊 ↦ ((2𝑜 ·𝑜 𝑤) +𝑜 𝑧))
23 infxpenc2.j . . . . . 6 𝐽 = (((ω CNF (2𝑜 ·𝑜 𝑊)) ∘ 𝐿) ∘ (ω CNF (𝑊 ·𝑜 2𝑜)))
24 infxpenc2.z . . . . . 6 𝑍 = (𝑥 ∈ (ω ↑𝑜 𝑊), 𝑦 ∈ (ω ↑𝑜 𝑊) ↦ (((ω ↑𝑜 𝑊) ·𝑜 𝑥) +𝑜 𝑦))
25 infxpenc2.t . . . . . 6 𝑇 = (𝑥𝑏, 𝑦𝑏 ↦ ⟨((𝑛𝑏)‘𝑥), ((𝑛𝑏)‘𝑦)⟩)
26 infxpenc2.g . . . . . 6 𝐺 = ((𝑛𝑏) ∘ (((𝐻𝐽) ∘ 𝑍) ∘ 𝑇))
277, 8, 12, 14, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26infxpenc 8786 . . . . 5 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → 𝐺:(𝑏 × 𝑏)–1-1-onto𝑏)
28 f1of 6096 . . . . . . . . 9 (𝐺:(𝑏 × 𝑏)–1-1-onto𝑏𝐺:(𝑏 × 𝑏)⟶𝑏)
2927, 28syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → 𝐺:(𝑏 × 𝑏)⟶𝑏)
30 vex 3194 . . . . . . . . 9 𝑏 ∈ V
3130, 30xpex 6916 . . . . . . . 8 (𝑏 × 𝑏) ∈ V
32 fex 6445 . . . . . . . 8 ((𝐺:(𝑏 × 𝑏)⟶𝑏 ∧ (𝑏 × 𝑏) ∈ V) → 𝐺 ∈ V)
3329, 31, 32sylancl 693 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → 𝐺 ∈ V)
34 eqid 2626 . . . . . . . 8 (𝑏𝐴𝐺) = (𝑏𝐴𝐺)
3534fvmpt2 6249 . . . . . . 7 ((𝑏𝐴𝐺 ∈ V) → ((𝑏𝐴𝐺)‘𝑏) = 𝐺)
365, 33, 35syl2anc 692 . . . . . 6 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → ((𝑏𝐴𝐺)‘𝑏) = 𝐺)
37 f1oeq1 6086 . . . . . 6 (((𝑏𝐴𝐺)‘𝑏) = 𝐺 → (((𝑏𝐴𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto𝑏𝐺:(𝑏 × 𝑏)–1-1-onto𝑏))
3836, 37syl 17 . . . . 5 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → (((𝑏𝐴𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto𝑏𝐺:(𝑏 × 𝑏)–1-1-onto𝑏))
3927, 38mpbird 247 . . . 4 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → ((𝑏𝐴𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)
4039expr 642 . . 3 ((𝜑𝑏𝐴) → (ω ⊆ 𝑏 → ((𝑏𝐴𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto𝑏))
4140ralrimiva 2965 . 2 (𝜑 → ∀𝑏𝐴 (ω ⊆ 𝑏 → ((𝑏𝐴𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto𝑏))
42 nfmpt1 4712 . . . . 5 𝑏(𝑏𝐴𝐺)
4342nfeq2 2782 . . . 4 𝑏 𝑔 = (𝑏𝐴𝐺)
44 fveq1 6149 . . . . . 6 (𝑔 = (𝑏𝐴𝐺) → (𝑔𝑏) = ((𝑏𝐴𝐺)‘𝑏))
45 f1oeq1 6086 . . . . . 6 ((𝑔𝑏) = ((𝑏𝐴𝐺)‘𝑏) → ((𝑔𝑏):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ ((𝑏𝐴𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto𝑏))
4644, 45syl 17 . . . . 5 (𝑔 = (𝑏𝐴𝐺) → ((𝑔𝑏):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ ((𝑏𝐴𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto𝑏))
4746imbi2d 330 . . . 4 (𝑔 = (𝑏𝐴𝐺) → ((ω ⊆ 𝑏 → (𝑔𝑏):(𝑏 × 𝑏)–1-1-onto𝑏) ↔ (ω ⊆ 𝑏 → ((𝑏𝐴𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)))
4843, 47ralbid 2982 . . 3 (𝑔 = (𝑏𝐴𝐺) → (∀𝑏𝐴 (ω ⊆ 𝑏 → (𝑔𝑏):(𝑏 × 𝑏)–1-1-onto𝑏) ↔ ∀𝑏𝐴 (ω ⊆ 𝑏 → ((𝑏𝐴𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)))
4948spcegv 3285 . 2 ((𝑏𝐴𝐺) ∈ V → (∀𝑏𝐴 (ω ⊆ 𝑏 → ((𝑏𝐴𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto𝑏) → ∃𝑔𝑏𝐴 (ω ⊆ 𝑏 → (𝑔𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)))
503, 41, 49sylc 65 1 (𝜑 → ∃𝑔𝑏𝐴 (ω ⊆ 𝑏 → (𝑔𝑏):(𝑏 × 𝑏)–1-1-onto𝑏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wex 1701  wcel 1992  wral 2912  wrex 2913  {crab 2916  Vcvv 3191  cdif 3557  wss 3560  c0 3896  cop 4159   class class class wbr 4618  cmpt 4678   I cid 4989   × cxp 5077  ccnv 5078  ran crn 5080  cres 5081  ccom 5083  Oncon0 5685  wf 5846  1-1-ontowf1o 5849  cfv 5850  (class class class)co 6605  cmpt2 6607  ωcom 7013  1𝑜c1o 7499  2𝑜c2o 7500   +𝑜 coa 7503   ·𝑜 comu 7504  𝑜 coe 7505  𝑚 cmap 7803   finSupp cfsupp 8220   CNF ccnf 8503
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-inf2 8483
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-isom 5859  df-riota 6566  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-om 7014  df-1st 7116  df-2nd 7117  df-supp 7242  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-seqom 7489  df-1o 7506  df-2o 7507  df-oadd 7510  df-omul 7511  df-oexp 7512  df-er 7688  df-map 7805  df-en 7901  df-dom 7902  df-sdom 7903  df-fin 7904  df-fsupp 8221  df-oi 8360  df-cnf 8504
This theorem is referenced by:  infxpenc2lem3  8789
  Copyright terms: Public domain W3C validator