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

Theorem isf32lem9 9221
 Description: Lemma for isfin3-2 9227. Construction of the onto function. (Contributed by Stefan O'Rear, 5-Nov-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
Hypotheses
Ref Expression
isf32lem.a (𝜑𝐹:ω⟶𝒫 𝐺)
isf32lem.b (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹𝑥))
isf32lem.c (𝜑 → ¬ ran 𝐹 ∈ ran 𝐹)
isf32lem.d 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹𝑦)}
isf32lem.e 𝐽 = (𝑢 ∈ ω ↦ (𝑣𝑆 (𝑣𝑆) ≈ 𝑢))
isf32lem.f 𝐾 = ((𝑤𝑆 ↦ ((𝐹𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)
isf32lem.g 𝐿 = (𝑡𝐺 ↦ (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾𝑠))))
Assertion
Ref Expression
isf32lem9 (𝜑𝐿:𝐺onto→ω)
Distinct variable groups:   𝑥,𝑤   𝑡,𝐺   𝑥,𝐿   𝑡,𝑠,𝑢,𝑣,𝑤,𝑥,𝑦,𝜑   𝑤,𝐹,𝑥,𝑦   𝑆,𝑠,𝑡,𝑢,𝑣,𝑤,𝑥,𝑦   𝐽,𝑠,𝑡,𝑤,𝑥,𝑦   𝐾,𝑠,𝑡,𝑥,𝑦
Allowed substitution hints:   𝐹(𝑣,𝑢,𝑡,𝑠)   𝐺(𝑥,𝑦,𝑤,𝑣,𝑢,𝑠)   𝐽(𝑣,𝑢)   𝐾(𝑤,𝑣,𝑢)   𝐿(𝑦,𝑤,𝑣,𝑢,𝑡,𝑠)

Proof of Theorem isf32lem9
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isf32lem.g . . . 4 𝐿 = (𝑡𝐺 ↦ (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾𝑠))))
2 ssab2 3719 . . . . . . 7 {𝑠 ∣ (𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾𝑠))} ⊆ ω
3 iotacl 5912 . . . . . . 7 (∃!𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾𝑠)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾𝑠))) ∈ {𝑠 ∣ (𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾𝑠))})
42, 3sseldi 3634 . . . . . 6 (∃!𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾𝑠)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾𝑠))) ∈ ω)
5 iotanul 5904 . . . . . . 7 (¬ ∃!𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾𝑠)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾𝑠))) = ∅)
6 peano1 7127 . . . . . . 7 ∅ ∈ ω
75, 6syl6eqel 2738 . . . . . 6 (¬ ∃!𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾𝑠)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾𝑠))) ∈ ω)
84, 7pm2.61i 176 . . . . 5 (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾𝑠))) ∈ ω
98a1i 11 . . . 4 (𝑡𝐺 → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾𝑠))) ∈ ω)
101, 9fmpti 6423 . . 3 𝐿:𝐺⟶ω
1110a1i 11 . 2 (𝜑𝐿:𝐺⟶ω)
12 isf32lem.a . . . . . 6 (𝜑𝐹:ω⟶𝒫 𝐺)
13 isf32lem.b . . . . . 6 (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹𝑥))
14 isf32lem.c . . . . . 6 (𝜑 → ¬ ran 𝐹 ∈ ran 𝐹)
15 isf32lem.d . . . . . 6 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹𝑦)}
16 isf32lem.e . . . . . 6 𝐽 = (𝑢 ∈ ω ↦ (𝑣𝑆 (𝑣𝑆) ≈ 𝑢))
17 isf32lem.f . . . . . 6 𝐾 = ((𝑤𝑆 ↦ ((𝐹𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)
1812, 13, 14, 15, 16, 17isf32lem6 9218 . . . . 5 ((𝜑𝑎 ∈ ω) → (𝐾𝑎) ≠ ∅)
19 n0 3964 . . . . 5 ((𝐾𝑎) ≠ ∅ ↔ ∃𝑏 𝑏 ∈ (𝐾𝑎))
2018, 19sylib 208 . . . 4 ((𝜑𝑎 ∈ ω) → ∃𝑏 𝑏 ∈ (𝐾𝑎))
2112, 13, 14, 15, 16, 17isf32lem8 9220 . . . . . . . . 9 ((𝜑𝑎 ∈ ω) → (𝐾𝑎) ⊆ 𝐺)
2221sselda 3636 . . . . . . . 8 (((𝜑𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾𝑎)) → 𝑏𝐺)
23 eleq1 2718 . . . . . . . . . . . . 13 (𝑡 = 𝑏 → (𝑡 ∈ (𝐾𝑠) ↔ 𝑏 ∈ (𝐾𝑠)))
2423anbi2d 740 . . . . . . . . . . . 12 (𝑡 = 𝑏 → ((𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾𝑠)) ↔ (𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾𝑠))))
2524iotabidv 5910 . . . . . . . . . . 11 (𝑡 = 𝑏 → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾𝑠))) = (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾𝑠))))
26 iotaex 5906 . . . . . . . . . . 11 (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾𝑠))) ∈ V
2725, 1, 26fvmpt3i 6326 . . . . . . . . . 10 (𝑏𝐺 → (𝐿𝑏) = (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾𝑠))))
2822, 27syl 17 . . . . . . . . 9 (((𝜑𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾𝑎)) → (𝐿𝑏) = (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾𝑠))))
29 simp1r 1106 . . . . . . . . . . . . . . . 16 (((𝜑𝑏 ∈ (𝐾𝑎)) ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → 𝑏 ∈ (𝐾𝑎))
30 simpl1 1084 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠𝑎) → 𝜑)
31 simpr 476 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠𝑎) → 𝑠𝑎)
3231necomd 2878 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠𝑎) → 𝑎𝑠)
33 simpl2 1085 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠𝑎) → 𝑎 ∈ ω)
34 simpl3 1086 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠𝑎) → 𝑠 ∈ ω)
3512, 13, 14, 15, 16, 17isf32lem7 9219 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑎𝑠) ∧ (𝑎 ∈ ω ∧ 𝑠 ∈ ω)) → ((𝐾𝑎) ∩ (𝐾𝑠)) = ∅)
3630, 32, 33, 34, 35syl22anc 1367 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠𝑎) → ((𝐾𝑎) ∩ (𝐾𝑠)) = ∅)
37 disj1 4052 . . . . . . . . . . . . . . . . . . . . 21 (((𝐾𝑎) ∩ (𝐾𝑠)) = ∅ ↔ ∀𝑏(𝑏 ∈ (𝐾𝑎) → ¬ 𝑏 ∈ (𝐾𝑠)))
3836, 37sylib 208 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠𝑎) → ∀𝑏(𝑏 ∈ (𝐾𝑎) → ¬ 𝑏 ∈ (𝐾𝑠)))
3938ex 449 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑠𝑎 → ∀𝑏(𝑏 ∈ (𝐾𝑎) → ¬ 𝑏 ∈ (𝐾𝑠))))
40 sp 2091 . . . . . . . . . . . . . . . . . . 19 (∀𝑏(𝑏 ∈ (𝐾𝑎) → ¬ 𝑏 ∈ (𝐾𝑠)) → (𝑏 ∈ (𝐾𝑎) → ¬ 𝑏 ∈ (𝐾𝑠)))
4139, 40syl6 35 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑠𝑎 → (𝑏 ∈ (𝐾𝑎) → ¬ 𝑏 ∈ (𝐾𝑠))))
4241com23 86 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑏 ∈ (𝐾𝑎) → (𝑠𝑎 → ¬ 𝑏 ∈ (𝐾𝑠))))
43423adant1r 1359 . . . . . . . . . . . . . . . 16 (((𝜑𝑏 ∈ (𝐾𝑎)) ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑏 ∈ (𝐾𝑎) → (𝑠𝑎 → ¬ 𝑏 ∈ (𝐾𝑠))))
4429, 43mpd 15 . . . . . . . . . . . . . . 15 (((𝜑𝑏 ∈ (𝐾𝑎)) ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑠𝑎 → ¬ 𝑏 ∈ (𝐾𝑠)))
4544necon4ad 2842 . . . . . . . . . . . . . 14 (((𝜑𝑏 ∈ (𝐾𝑎)) ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑏 ∈ (𝐾𝑠) → 𝑠 = 𝑎))
46453expia 1286 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (𝐾𝑎)) ∧ 𝑎 ∈ ω) → (𝑠 ∈ ω → (𝑏 ∈ (𝐾𝑠) → 𝑠 = 𝑎)))
4746impd 446 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (𝐾𝑎)) ∧ 𝑎 ∈ ω) → ((𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾𝑠)) → 𝑠 = 𝑎))
48 eleq1 2718 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑎 → (𝑠 ∈ ω ↔ 𝑎 ∈ ω))
49 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑠 = 𝑎 → (𝐾𝑠) = (𝐾𝑎))
5049eleq2d 2716 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑎 → (𝑏 ∈ (𝐾𝑠) ↔ 𝑏 ∈ (𝐾𝑎)))
5148, 50anbi12d 747 . . . . . . . . . . . . . . 15 (𝑠 = 𝑎 → ((𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾𝑠)) ↔ (𝑎 ∈ ω ∧ 𝑏 ∈ (𝐾𝑎))))
5251biimprcd 240 . . . . . . . . . . . . . 14 ((𝑎 ∈ ω ∧ 𝑏 ∈ (𝐾𝑎)) → (𝑠 = 𝑎 → (𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾𝑠))))
5352ancoms 468 . . . . . . . . . . . . 13 ((𝑏 ∈ (𝐾𝑎) ∧ 𝑎 ∈ ω) → (𝑠 = 𝑎 → (𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾𝑠))))
5453adantll 750 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (𝐾𝑎)) ∧ 𝑎 ∈ ω) → (𝑠 = 𝑎 → (𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾𝑠))))
5547, 54impbid 202 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (𝐾𝑎)) ∧ 𝑎 ∈ ω) → ((𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾𝑠)) ↔ 𝑠 = 𝑎))
5655iota5 5909 . . . . . . . . . 10 (((𝜑𝑏 ∈ (𝐾𝑎)) ∧ 𝑎 ∈ ω) → (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾𝑠))) = 𝑎)
5756an32s 863 . . . . . . . . 9 (((𝜑𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾𝑎)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾𝑠))) = 𝑎)
5828, 57eqtr2d 2686 . . . . . . . 8 (((𝜑𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾𝑎)) → 𝑎 = (𝐿𝑏))
5922, 58jca 553 . . . . . . 7 (((𝜑𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾𝑎)) → (𝑏𝐺𝑎 = (𝐿𝑏)))
6059ex 449 . . . . . 6 ((𝜑𝑎 ∈ ω) → (𝑏 ∈ (𝐾𝑎) → (𝑏𝐺𝑎 = (𝐿𝑏))))
6160eximdv 1886 . . . . 5 ((𝜑𝑎 ∈ ω) → (∃𝑏 𝑏 ∈ (𝐾𝑎) → ∃𝑏(𝑏𝐺𝑎 = (𝐿𝑏))))
62 df-rex 2947 . . . . 5 (∃𝑏𝐺 𝑎 = (𝐿𝑏) ↔ ∃𝑏(𝑏𝐺𝑎 = (𝐿𝑏)))
6361, 62syl6ibr 242 . . . 4 ((𝜑𝑎 ∈ ω) → (∃𝑏 𝑏 ∈ (𝐾𝑎) → ∃𝑏𝐺 𝑎 = (𝐿𝑏)))
6420, 63mpd 15 . . 3 ((𝜑𝑎 ∈ ω) → ∃𝑏𝐺 𝑎 = (𝐿𝑏))
6564ralrimiva 2995 . 2 (𝜑 → ∀𝑎 ∈ ω ∃𝑏𝐺 𝑎 = (𝐿𝑏))
66 dffo3 6414 . 2 (𝐿:𝐺onto→ω ↔ (𝐿:𝐺⟶ω ∧ ∀𝑎 ∈ ω ∃𝑏𝐺 𝑎 = (𝐿𝑏)))
6711, 65, 66sylanbrc 699 1 (𝜑𝐿:𝐺onto→ω)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∧ w3a 1054  ∀wal 1521   = wceq 1523  ∃wex 1744   ∈ wcel 2030  ∃!weu 2498  {cab 2637   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  {crab 2945   ∖ cdif 3604   ∩ cin 3606   ⊆ wss 3607   ⊊ wpss 3608  ∅c0 3948  𝒫 cpw 4191  ∩ cint 4507   class class class wbr 4685   ↦ cmpt 4762  ran crn 5144   ∘ ccom 5147  suc csuc 5763  ℩cio 5887  ⟶wf 5922  –onto→wfo 5924  ‘cfv 5926  ℩crio 6650  ωcom 7107   ≈ cen 7994 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-om 7108  df-wrecs 7452  df-recs 7513  df-1o 7605  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803 This theorem is referenced by:  isf32lem10  9222
 Copyright terms: Public domain W3C validator