Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  axccdom Structured version   Visualization version   GIF version

Theorem axccdom 43379
Description: Relax the constraint on ax-cc to dominance instead of equinumerosity. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Hypotheses
Ref Expression
axccdom.1 (𝜑𝑋 ≼ ω)
axccdom.2 ((𝜑𝑧𝑋) → 𝑧 ≠ ∅)
Assertion
Ref Expression
axccdom (𝜑 → ∃𝑓(𝑓 Fn 𝑋 ∧ ∀𝑧𝑋 (𝑓𝑧) ∈ 𝑧))
Distinct variable groups:   𝑓,𝑋,𝑧   𝜑,𝑧
Allowed substitution hint:   𝜑(𝑓)

Proof of Theorem axccdom
Dummy variables 𝑔 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 485 . . 3 ((𝜑𝑋 ∈ Fin) → 𝑋 ∈ Fin)
2 simpr 485 . . 3 (((𝜑𝑋 ∈ Fin) ∧ 𝑧𝑋) → 𝑧𝑋)
3 axccdom.2 . . . 4 ((𝜑𝑧𝑋) → 𝑧 ≠ ∅)
43adantlr 713 . . 3 (((𝜑𝑋 ∈ Fin) ∧ 𝑧𝑋) → 𝑧 ≠ ∅)
51, 2, 4choicefi 43357 . 2 ((𝜑𝑋 ∈ Fin) → ∃𝑓(𝑓 Fn 𝑋 ∧ ∀𝑧𝑋 (𝑓𝑧) ∈ 𝑧))
6 axccdom.1 . . . . . 6 (𝜑𝑋 ≼ ω)
76adantr 481 . . . . 5 ((𝜑 ∧ ¬ 𝑋 ∈ Fin) → 𝑋 ≼ ω)
8 isfinite2 9241 . . . . . . 7 (𝑋 ≺ ω → 𝑋 ∈ Fin)
98con3i 154 . . . . . 6 𝑋 ∈ Fin → ¬ 𝑋 ≺ ω)
109adantl 482 . . . . 5 ((𝜑 ∧ ¬ 𝑋 ∈ Fin) → ¬ 𝑋 ≺ ω)
117, 10jca 512 . . . 4 ((𝜑 ∧ ¬ 𝑋 ∈ Fin) → (𝑋 ≼ ω ∧ ¬ 𝑋 ≺ ω))
12 bren2 8919 . . . 4 (𝑋 ≈ ω ↔ (𝑋 ≼ ω ∧ ¬ 𝑋 ≺ ω))
1311, 12sylibr 233 . . 3 ((𝜑 ∧ ¬ 𝑋 ∈ Fin) → 𝑋 ≈ ω)
14 ctex 8899 . . . . . . 7 (𝑋 ≼ ω → 𝑋 ∈ V)
156, 14syl 17 . . . . . 6 (𝜑𝑋 ∈ V)
1615adantr 481 . . . . 5 ((𝜑𝑋 ≈ ω) → 𝑋 ∈ V)
17 simpr 485 . . . . 5 ((𝜑𝑋 ≈ ω) → 𝑋 ≈ ω)
18 breq1 5106 . . . . . . 7 (𝑥 = 𝑋 → (𝑥 ≈ ω ↔ 𝑋 ≈ ω))
19 raleq 3307 . . . . . . . 8 (𝑥 = 𝑋 → (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧) ↔ ∀𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧)))
2019exbidv 1924 . . . . . . 7 (𝑥 = 𝑋 → (∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧) ↔ ∃𝑔𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧)))
2118, 20imbi12d 344 . . . . . 6 (𝑥 = 𝑋 → ((𝑥 ≈ ω → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧)) ↔ (𝑋 ≈ ω → ∃𝑔𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))))
22 ax-cc 10367 . . . . . 6 (𝑥 ≈ ω → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
2321, 22vtoclg 3523 . . . . 5 (𝑋 ∈ V → (𝑋 ≈ ω → ∃𝑔𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧)))
2416, 17, 23sylc 65 . . . 4 ((𝜑𝑋 ≈ ω) → ∃𝑔𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
2515mptexd 7170 . . . . . . . . 9 (𝜑 → (𝑧𝑋 ↦ (𝑔𝑧)) ∈ V)
2625adantr 481 . . . . . . . 8 ((𝜑 ∧ ∀𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧)) → (𝑧𝑋 ↦ (𝑔𝑧)) ∈ V)
27 fvex 6852 . . . . . . . . . . . 12 (𝑔𝑧) ∈ V
2827rgenw 3066 . . . . . . . . . . 11 𝑧𝑋 (𝑔𝑧) ∈ V
29 eqid 2736 . . . . . . . . . . . 12 (𝑧𝑋 ↦ (𝑔𝑧)) = (𝑧𝑋 ↦ (𝑔𝑧))
3029fnmpt 6638 . . . . . . . . . . 11 (∀𝑧𝑋 (𝑔𝑧) ∈ V → (𝑧𝑋 ↦ (𝑔𝑧)) Fn 𝑋)
3128, 30ax-mp 5 . . . . . . . . . 10 (𝑧𝑋 ↦ (𝑔𝑧)) Fn 𝑋
3231a1i 11 . . . . . . . . 9 ((𝜑 ∧ ∀𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧)) → (𝑧𝑋 ↦ (𝑔𝑧)) Fn 𝑋)
33 nfv 1917 . . . . . . . . . . 11 𝑧𝜑
34 nfra1 3265 . . . . . . . . . . 11 𝑧𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧)
3533, 34nfan 1902 . . . . . . . . . 10 𝑧(𝜑 ∧ ∀𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
36 id 22 . . . . . . . . . . . . . 14 (𝑧𝑋𝑧𝑋)
3727a1i 11 . . . . . . . . . . . . . 14 (𝑧𝑋 → (𝑔𝑧) ∈ V)
3829fvmpt2 6956 . . . . . . . . . . . . . 14 ((𝑧𝑋 ∧ (𝑔𝑧) ∈ V) → ((𝑧𝑋 ↦ (𝑔𝑧))‘𝑧) = (𝑔𝑧))
3936, 37, 38syl2anc 584 . . . . . . . . . . . . 13 (𝑧𝑋 → ((𝑧𝑋 ↦ (𝑔𝑧))‘𝑧) = (𝑔𝑧))
4039adantl 482 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧)) ∧ 𝑧𝑋) → ((𝑧𝑋 ↦ (𝑔𝑧))‘𝑧) = (𝑔𝑧))
41 rspa 3229 . . . . . . . . . . . . . 14 ((∀𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧) ∧ 𝑧𝑋) → (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
4241adantll 712 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧)) ∧ 𝑧𝑋) → (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
433adantlr 713 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧)) ∧ 𝑧𝑋) → 𝑧 ≠ ∅)
44 id 22 . . . . . . . . . . . . 13 ((𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧) → (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
4542, 43, 44sylc 65 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧)) ∧ 𝑧𝑋) → (𝑔𝑧) ∈ 𝑧)
4640, 45eqeltrd 2838 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧)) ∧ 𝑧𝑋) → ((𝑧𝑋 ↦ (𝑔𝑧))‘𝑧) ∈ 𝑧)
4746ex 413 . . . . . . . . . 10 ((𝜑 ∧ ∀𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧)) → (𝑧𝑋 → ((𝑧𝑋 ↦ (𝑔𝑧))‘𝑧) ∈ 𝑧))
4835, 47ralrimi 3238 . . . . . . . . 9 ((𝜑 ∧ ∀𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧)) → ∀𝑧𝑋 ((𝑧𝑋 ↦ (𝑔𝑧))‘𝑧) ∈ 𝑧)
4932, 48jca 512 . . . . . . . 8 ((𝜑 ∧ ∀𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧)) → ((𝑧𝑋 ↦ (𝑔𝑧)) Fn 𝑋 ∧ ∀𝑧𝑋 ((𝑧𝑋 ↦ (𝑔𝑧))‘𝑧) ∈ 𝑧))
50 fneq1 6590 . . . . . . . . . 10 (𝑓 = (𝑧𝑋 ↦ (𝑔𝑧)) → (𝑓 Fn 𝑋 ↔ (𝑧𝑋 ↦ (𝑔𝑧)) Fn 𝑋))
51 nfcv 2905 . . . . . . . . . . . 12 𝑧𝑓
52 nfmpt1 5211 . . . . . . . . . . . 12 𝑧(𝑧𝑋 ↦ (𝑔𝑧))
5351, 52nfeq 2918 . . . . . . . . . . 11 𝑧 𝑓 = (𝑧𝑋 ↦ (𝑔𝑧))
54 fveq1 6838 . . . . . . . . . . . 12 (𝑓 = (𝑧𝑋 ↦ (𝑔𝑧)) → (𝑓𝑧) = ((𝑧𝑋 ↦ (𝑔𝑧))‘𝑧))
5554eleq1d 2822 . . . . . . . . . . 11 (𝑓 = (𝑧𝑋 ↦ (𝑔𝑧)) → ((𝑓𝑧) ∈ 𝑧 ↔ ((𝑧𝑋 ↦ (𝑔𝑧))‘𝑧) ∈ 𝑧))
5653, 55ralbid 3254 . . . . . . . . . 10 (𝑓 = (𝑧𝑋 ↦ (𝑔𝑧)) → (∀𝑧𝑋 (𝑓𝑧) ∈ 𝑧 ↔ ∀𝑧𝑋 ((𝑧𝑋 ↦ (𝑔𝑧))‘𝑧) ∈ 𝑧))
5750, 56anbi12d 631 . . . . . . . . 9 (𝑓 = (𝑧𝑋 ↦ (𝑔𝑧)) → ((𝑓 Fn 𝑋 ∧ ∀𝑧𝑋 (𝑓𝑧) ∈ 𝑧) ↔ ((𝑧𝑋 ↦ (𝑔𝑧)) Fn 𝑋 ∧ ∀𝑧𝑋 ((𝑧𝑋 ↦ (𝑔𝑧))‘𝑧) ∈ 𝑧)))
5857spcegv 3554 . . . . . . . 8 ((𝑧𝑋 ↦ (𝑔𝑧)) ∈ V → (((𝑧𝑋 ↦ (𝑔𝑧)) Fn 𝑋 ∧ ∀𝑧𝑋 ((𝑧𝑋 ↦ (𝑔𝑧))‘𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑋 ∧ ∀𝑧𝑋 (𝑓𝑧) ∈ 𝑧)))
5926, 49, 58sylc 65 . . . . . . 7 ((𝜑 ∧ ∀𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧)) → ∃𝑓(𝑓 Fn 𝑋 ∧ ∀𝑧𝑋 (𝑓𝑧) ∈ 𝑧))
6059adantlr 713 . . . . . 6 (((𝜑𝑋 ≈ ω) ∧ ∀𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧)) → ∃𝑓(𝑓 Fn 𝑋 ∧ ∀𝑧𝑋 (𝑓𝑧) ∈ 𝑧))
6160ex 413 . . . . 5 ((𝜑𝑋 ≈ ω) → (∀𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑋 ∧ ∀𝑧𝑋 (𝑓𝑧) ∈ 𝑧)))
6261exlimdv 1936 . . . 4 ((𝜑𝑋 ≈ ω) → (∃𝑔𝑧𝑋 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧) → ∃𝑓(𝑓 Fn 𝑋 ∧ ∀𝑧𝑋 (𝑓𝑧) ∈ 𝑧)))
6324, 62mpd 15 . . 3 ((𝜑𝑋 ≈ ω) → ∃𝑓(𝑓 Fn 𝑋 ∧ ∀𝑧𝑋 (𝑓𝑧) ∈ 𝑧))
6413, 63syldan 591 . 2 ((𝜑 ∧ ¬ 𝑋 ∈ Fin) → ∃𝑓(𝑓 Fn 𝑋 ∧ ∀𝑧𝑋 (𝑓𝑧) ∈ 𝑧))
655, 64pm2.61dan 811 1 (𝜑 → ∃𝑓(𝑓 Fn 𝑋 ∧ ∀𝑧𝑋 (𝑓𝑧) ∈ 𝑧))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1541  wex 1781  wcel 2106  wne 2941  wral 3062  Vcvv 3443  c0 4280   class class class wbr 5103  cmpt 5186   Fn wfn 6488  cfv 6493  ωcom 7798  cen 8876  cdom 8877  csdm 8878  Fincfn 8879
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7668  ax-cc 10367
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7356  df-om 7799  df-1st 7917  df-2nd 7918  df-frecs 8208  df-wrecs 8239  df-recs 8313  df-rdg 8352  df-1o 8408  df-er 8644  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883
This theorem is referenced by:  subsaliuncl  44531
  Copyright terms: Public domain W3C validator