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

Theorem infxpenc2lem2 9444
Description: Lemma for infxpenc2 9446. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 7-Jul-2019.)
Hypotheses
Ref Expression
infxpenc2.1 (𝜑𝐴 ∈ On)
infxpenc2.2 (𝜑 → ∀𝑏𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑛𝑏):𝑏1-1-onto→(ω ↑o 𝑤)))
infxpenc2.3 𝑊 = ((𝑥 ∈ (On ∖ 1o) ↦ (ω ↑o 𝑥))‘ran (𝑛𝑏))
infxpenc2.4 (𝜑𝐹:(ω ↑o 2o)–1-1-onto→ω)
infxpenc2.5 (𝜑 → (𝐹‘∅) = ∅)
infxpenc2.k 𝐾 = (𝑦 ∈ {𝑥 ∈ ((ω ↑o 2o) ↑m 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦( I ↾ 𝑊))))
infxpenc2.h 𝐻 = (((ω CNF 𝑊) ∘ 𝐾) ∘ ((ω ↑o 2o) CNF 𝑊))
infxpenc2.l 𝐿 = (𝑦 ∈ {𝑥 ∈ (ω ↑m (𝑊 ·o 2o)) ∣ 𝑥 finSupp ∅} ↦ (( I ↾ ω) ∘ (𝑦(𝑌𝑋))))
infxpenc2.x 𝑋 = (𝑧 ∈ 2o, 𝑤𝑊 ↦ ((𝑊 ·o 𝑧) +o 𝑤))
infxpenc2.y 𝑌 = (𝑧 ∈ 2o, 𝑤𝑊 ↦ ((2o ·o 𝑤) +o 𝑧))
infxpenc2.j 𝐽 = (((ω CNF (2o ·o 𝑊)) ∘ 𝐿) ∘ (ω CNF (𝑊 ·o 2o)))
infxpenc2.z 𝑍 = (𝑥 ∈ (ω ↑o 𝑊), 𝑦 ∈ (ω ↑o 𝑊) ↦ (((ω ↑o 𝑊) ·o 𝑥) +o 𝑦))
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)
21mptexd 6978 . 2 (𝜑 → (𝑏𝐴𝐺) ∈ V)
31adantr 484 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → 𝐴 ∈ On)
4 simprl 770 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → 𝑏𝐴)
5 onelon 6203 . . . . . . 7 ((𝐴 ∈ On ∧ 𝑏𝐴) → 𝑏 ∈ On)
63, 4, 5syl2anc 587 . . . . . 6 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → 𝑏 ∈ On)
7 simprr 772 . . . . . 6 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → ω ⊆ 𝑏)
8 infxpenc2.2 . . . . . . . 8 (𝜑 → ∀𝑏𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑛𝑏):𝑏1-1-onto→(ω ↑o 𝑤)))
9 infxpenc2.3 . . . . . . . 8 𝑊 = ((𝑥 ∈ (On ∖ 1o) ↦ (ω ↑o 𝑥))‘ran (𝑛𝑏))
101, 8, 9infxpenc2lem1 9443 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → (𝑊 ∈ (On ∖ 1o) ∧ (𝑛𝑏):𝑏1-1-onto→(ω ↑o 𝑊)))
1110simpld 498 . . . . . 6 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → 𝑊 ∈ (On ∖ 1o))
12 infxpenc2.4 . . . . . . 7 (𝜑𝐹:(ω ↑o 2o)–1-1-onto→ω)
1312adantr 484 . . . . . 6 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → 𝐹:(ω ↑o 2o)–1-1-onto→ω)
14 infxpenc2.5 . . . . . . 7 (𝜑 → (𝐹‘∅) = ∅)
1514adantr 484 . . . . . 6 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → (𝐹‘∅) = ∅)
1610simprd 499 . . . . . 6 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → (𝑛𝑏):𝑏1-1-onto→(ω ↑o 𝑊))
17 infxpenc2.k . . . . . 6 𝐾 = (𝑦 ∈ {𝑥 ∈ ((ω ↑o 2o) ↑m 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦( I ↾ 𝑊))))
18 infxpenc2.h . . . . . 6 𝐻 = (((ω CNF 𝑊) ∘ 𝐾) ∘ ((ω ↑o 2o) CNF 𝑊))
19 infxpenc2.l . . . . . 6 𝐿 = (𝑦 ∈ {𝑥 ∈ (ω ↑m (𝑊 ·o 2o)) ∣ 𝑥 finSupp ∅} ↦ (( I ↾ ω) ∘ (𝑦(𝑌𝑋))))
20 infxpenc2.x . . . . . 6 𝑋 = (𝑧 ∈ 2o, 𝑤𝑊 ↦ ((𝑊 ·o 𝑧) +o 𝑤))
21 infxpenc2.y . . . . . 6 𝑌 = (𝑧 ∈ 2o, 𝑤𝑊 ↦ ((2o ·o 𝑤) +o 𝑧))
22 infxpenc2.j . . . . . 6 𝐽 = (((ω CNF (2o ·o 𝑊)) ∘ 𝐿) ∘ (ω CNF (𝑊 ·o 2o)))
23 infxpenc2.z . . . . . 6 𝑍 = (𝑥 ∈ (ω ↑o 𝑊), 𝑦 ∈ (ω ↑o 𝑊) ↦ (((ω ↑o 𝑊) ·o 𝑥) +o 𝑦))
24 infxpenc2.t . . . . . 6 𝑇 = (𝑥𝑏, 𝑦𝑏 ↦ ⟨((𝑛𝑏)‘𝑥), ((𝑛𝑏)‘𝑦)⟩)
25 infxpenc2.g . . . . . 6 𝐺 = ((𝑛𝑏) ∘ (((𝐻𝐽) ∘ 𝑍) ∘ 𝑇))
266, 7, 11, 13, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25infxpenc 9442 . . . . 5 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → 𝐺:(𝑏 × 𝑏)–1-1-onto𝑏)
27 f1of 6606 . . . . . . . . 9 (𝐺:(𝑏 × 𝑏)–1-1-onto𝑏𝐺:(𝑏 × 𝑏)⟶𝑏)
2826, 27syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → 𝐺:(𝑏 × 𝑏)⟶𝑏)
29 vex 3483 . . . . . . . . 9 𝑏 ∈ V
3029, 29xpex 7470 . . . . . . . 8 (𝑏 × 𝑏) ∈ V
31 fex 6980 . . . . . . . 8 ((𝐺:(𝑏 × 𝑏)⟶𝑏 ∧ (𝑏 × 𝑏) ∈ V) → 𝐺 ∈ V)
3228, 30, 31sylancl 589 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → 𝐺 ∈ V)
33 eqid 2824 . . . . . . . 8 (𝑏𝐴𝐺) = (𝑏𝐴𝐺)
3433fvmpt2 6770 . . . . . . 7 ((𝑏𝐴𝐺 ∈ V) → ((𝑏𝐴𝐺)‘𝑏) = 𝐺)
354, 32, 34syl2anc 587 . . . . . 6 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → ((𝑏𝐴𝐺)‘𝑏) = 𝐺)
36 f1oeq1 6595 . . . . . 6 (((𝑏𝐴𝐺)‘𝑏) = 𝐺 → (((𝑏𝐴𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto𝑏𝐺:(𝑏 × 𝑏)–1-1-onto𝑏))
3735, 36syl 17 . . . . 5 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → (((𝑏𝐴𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto𝑏𝐺:(𝑏 × 𝑏)–1-1-onto𝑏))
3826, 37mpbird 260 . . . 4 ((𝜑 ∧ (𝑏𝐴 ∧ ω ⊆ 𝑏)) → ((𝑏𝐴𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)
3938expr 460 . . 3 ((𝜑𝑏𝐴) → (ω ⊆ 𝑏 → ((𝑏𝐴𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto𝑏))
4039ralrimiva 3177 . 2 (𝜑 → ∀𝑏𝐴 (ω ⊆ 𝑏 → ((𝑏𝐴𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto𝑏))
41 nfmpt1 5150 . . . 4 𝑏(𝑏𝐴𝐺)
4241nfeq2 2999 . . 3 𝑏 𝑔 = (𝑏𝐴𝐺)
43 fveq1 6660 . . . . 5 (𝑔 = (𝑏𝐴𝐺) → (𝑔𝑏) = ((𝑏𝐴𝐺)‘𝑏))
44 f1oeq1 6595 . . . . 5 ((𝑔𝑏) = ((𝑏𝐴𝐺)‘𝑏) → ((𝑔𝑏):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ ((𝑏𝐴𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto𝑏))
4543, 44syl 17 . . . 4 (𝑔 = (𝑏𝐴𝐺) → ((𝑔𝑏):(𝑏 × 𝑏)–1-1-onto𝑏 ↔ ((𝑏𝐴𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto𝑏))
4645imbi2d 344 . . 3 (𝑔 = (𝑏𝐴𝐺) → ((ω ⊆ 𝑏 → (𝑔𝑏):(𝑏 × 𝑏)–1-1-onto𝑏) ↔ (ω ⊆ 𝑏 → ((𝑏𝐴𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)))
4742, 46ralbid 3225 . 2 (𝑔 = (𝑏𝐴𝐺) → (∀𝑏𝐴 (ω ⊆ 𝑏 → (𝑔𝑏):(𝑏 × 𝑏)–1-1-onto𝑏) ↔ ∀𝑏𝐴 (ω ⊆ 𝑏 → ((𝑏𝐴𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto𝑏)))
482, 40, 47spcedv 3585 1 (𝜑 → ∃𝑔𝑏𝐴 (ω ⊆ 𝑏 → (𝑔𝑏):(𝑏 × 𝑏)–1-1-onto𝑏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wex 1781  wcel 2115  wral 3133  wrex 3134  {crab 3137  Vcvv 3480  cdif 3916  wss 3919  c0 4276  cop 4556   class class class wbr 5052  cmpt 5132   I cid 5446   × cxp 5540  ccnv 5541  ran crn 5543  cres 5544  ccom 5546  Oncon0 6178  wf 6339  1-1-ontowf1o 6342  cfv 6343  (class class class)co 7149  cmpo 7151  ωcom 7574  1oc1o 8091  2oc2o 8092   +o coa 8095   ·o comu 8096  o coe 8097  m cmap 8402   finSupp cfsupp 8830   CNF ccnf 9121
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-inf2 9101
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-om 7575  df-1st 7684  df-2nd 7685  df-supp 7827  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-seqom 8080  df-1o 8098  df-2o 8099  df-oadd 8102  df-omul 8103  df-oexp 8104  df-er 8285  df-map 8404  df-en 8506  df-dom 8507  df-sdom 8508  df-fin 8509  df-fsupp 8831  df-oi 8971  df-cnf 9122
This theorem is referenced by:  infxpenc2lem3  9445
  Copyright terms: Public domain W3C validator