Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dfac21 Structured version   Visualization version   GIF version

Theorem dfac21 40602
Description: Tychonoff's theorem is a choice equivalent. Definition AC21 of Schechter p. 461. (Contributed by Stefan O'Rear, 22-Feb-2015.) (Revised by Mario Carneiro, 27-Aug-2015.)
Assertion
Ref Expression
dfac21 (CHOICE ↔ ∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t𝑓) ∈ Comp))

Proof of Theorem dfac21
Dummy variables 𝑔 𝑦 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3417 . . . . . . 7 𝑓 ∈ V
21dmex 7694 . . . . . 6 dom 𝑓 ∈ V
32a1i 11 . . . . 5 ((CHOICE𝑓:dom 𝑓⟶Comp) → dom 𝑓 ∈ V)
4 simpr 488 . . . . 5 ((CHOICE𝑓:dom 𝑓⟶Comp) → 𝑓:dom 𝑓⟶Comp)
5 fvex 6735 . . . . . . . 8 (∏t𝑓) ∈ V
65uniex 7534 . . . . . . 7 (∏t𝑓) ∈ V
7 acufl 22819 . . . . . . . 8 (CHOICE → UFL = V)
87adantr 484 . . . . . . 7 ((CHOICE𝑓:dom 𝑓⟶Comp) → UFL = V)
96, 8eleqtrrid 2845 . . . . . 6 ((CHOICE𝑓:dom 𝑓⟶Comp) → (∏t𝑓) ∈ UFL)
10 simpl 486 . . . . . . . 8 ((CHOICE𝑓:dom 𝑓⟶Comp) → CHOICE)
11 dfac10 9756 . . . . . . . 8 (CHOICE ↔ dom card = V)
1210, 11sylib 221 . . . . . . 7 ((CHOICE𝑓:dom 𝑓⟶Comp) → dom card = V)
136, 12eleqtrrid 2845 . . . . . 6 ((CHOICE𝑓:dom 𝑓⟶Comp) → (∏t𝑓) ∈ dom card)
149, 13elind 4113 . . . . 5 ((CHOICE𝑓:dom 𝑓⟶Comp) → (∏t𝑓) ∈ (UFL ∩ dom card))
15 eqid 2737 . . . . . 6 (∏t𝑓) = (∏t𝑓)
16 eqid 2737 . . . . . 6 (∏t𝑓) = (∏t𝑓)
1715, 16ptcmpg 22959 . . . . 5 ((dom 𝑓 ∈ V ∧ 𝑓:dom 𝑓⟶Comp ∧ (∏t𝑓) ∈ (UFL ∩ dom card)) → (∏t𝑓) ∈ Comp)
183, 4, 14, 17syl3anc 1373 . . . 4 ((CHOICE𝑓:dom 𝑓⟶Comp) → (∏t𝑓) ∈ Comp)
1918ex 416 . . 3 (CHOICE → (𝑓:dom 𝑓⟶Comp → (∏t𝑓) ∈ Comp))
2019alrimiv 1935 . 2 (CHOICE → ∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t𝑓) ∈ Comp))
21 fvex 6735 . . . . . . . . 9 (𝑔𝑦) ∈ V
22 kelac2lem 40600 . . . . . . . . 9 ((𝑔𝑦) ∈ V → (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}) ∈ Comp)
2321, 22mp1i 13 . . . . . . . 8 (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑦 ∈ dom 𝑔) → (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}) ∈ Comp)
2423fmpttd 6937 . . . . . . 7 ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}})):dom 𝑔⟶Comp)
2524ffdmd 6581 . . . . . 6 ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}})):dom (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}))⟶Comp)
26 vex 3417 . . . . . . . . 9 𝑔 ∈ V
2726dmex 7694 . . . . . . . 8 dom 𝑔 ∈ V
2827mptex 7044 . . . . . . 7 (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}})) ∈ V
29 id 22 . . . . . . . . 9 (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}})) → 𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}})))
30 dmeq 5777 . . . . . . . . 9 (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}})) → dom 𝑓 = dom (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}})))
3129, 30feq12d 6538 . . . . . . . 8 (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}})) → (𝑓:dom 𝑓⟶Comp ↔ (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}})):dom (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}))⟶Comp))
32 fveq2 6722 . . . . . . . . 9 (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}})) → (∏t𝑓) = (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}))))
3332eleq1d 2822 . . . . . . . 8 (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}})) → ((∏t𝑓) ∈ Comp ↔ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}))) ∈ Comp))
3431, 33imbi12d 348 . . . . . . 7 (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}})) → ((𝑓:dom 𝑓⟶Comp → (∏t𝑓) ∈ Comp) ↔ ((𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}})):dom (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}))⟶Comp → (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}))) ∈ Comp)))
3528, 34spcv 3525 . . . . . 6 (∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t𝑓) ∈ Comp) → ((𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}})):dom (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}))⟶Comp → (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}))) ∈ Comp))
3625, 35syl5com 31 . . . . 5 ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → (∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t𝑓) ∈ Comp) → (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}))) ∈ Comp))
37 fvex 6735 . . . . . . . 8 (𝑔𝑥) ∈ V
3837a1i 11 . . . . . . 7 ((((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}))) ∈ Comp) ∧ 𝑥 ∈ dom 𝑔) → (𝑔𝑥) ∈ V)
39 df-nel 3047 . . . . . . . . . . 11 (∅ ∉ ran 𝑔 ↔ ¬ ∅ ∈ ran 𝑔)
4039biimpi 219 . . . . . . . . . 10 (∅ ∉ ran 𝑔 → ¬ ∅ ∈ ran 𝑔)
4140ad2antlr 727 . . . . . . . . 9 (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → ¬ ∅ ∈ ran 𝑔)
42 fvelrn 6902 . . . . . . . . . . . 12 ((Fun 𝑔𝑥 ∈ dom 𝑔) → (𝑔𝑥) ∈ ran 𝑔)
4342adantlr 715 . . . . . . . . . . 11 (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → (𝑔𝑥) ∈ ran 𝑔)
44 eleq1 2825 . . . . . . . . . . 11 ((𝑔𝑥) = ∅ → ((𝑔𝑥) ∈ ran 𝑔 ↔ ∅ ∈ ran 𝑔))
4543, 44syl5ibcom 248 . . . . . . . . . 10 (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → ((𝑔𝑥) = ∅ → ∅ ∈ ran 𝑔))
4645necon3bd 2954 . . . . . . . . 9 (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → (¬ ∅ ∈ ran 𝑔 → (𝑔𝑥) ≠ ∅))
4741, 46mpd 15 . . . . . . . 8 (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → (𝑔𝑥) ≠ ∅)
4847adantlr 715 . . . . . . 7 ((((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}))) ∈ Comp) ∧ 𝑥 ∈ dom 𝑔) → (𝑔𝑥) ≠ ∅)
49 fveq2 6722 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (𝑔𝑦) = (𝑔𝑥))
5049unieqd 4838 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑥 (𝑔𝑦) = (𝑔𝑥))
5150pweqd 4537 . . . . . . . . . . . . . . 15 (𝑦 = 𝑥 → 𝒫 (𝑔𝑦) = 𝒫 (𝑔𝑥))
5251sneqd 4558 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → {𝒫 (𝑔𝑦)} = {𝒫 (𝑔𝑥)})
5349, 52preq12d 4662 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → {(𝑔𝑦), {𝒫 (𝑔𝑦)}} = {(𝑔𝑥), {𝒫 (𝑔𝑥)}})
5453fveq2d 6726 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}) = (topGen‘{(𝑔𝑥), {𝒫 (𝑔𝑥)}}))
5554cbvmptv 5163 . . . . . . . . . . 11 (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}})) = (𝑥 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑥), {𝒫 (𝑔𝑥)}}))
5655fveq2i 6725 . . . . . . . . . 10 (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}))) = (∏t‘(𝑥 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑥), {𝒫 (𝑔𝑥)}})))
5756eleq1i 2828 . . . . . . . . 9 ((∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}))) ∈ Comp ↔ (∏t‘(𝑥 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑥), {𝒫 (𝑔𝑥)}}))) ∈ Comp)
5857biimpi 219 . . . . . . . 8 ((∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}))) ∈ Comp → (∏t‘(𝑥 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑥), {𝒫 (𝑔𝑥)}}))) ∈ Comp)
5958adantl 485 . . . . . . 7 (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}))) ∈ Comp) → (∏t‘(𝑥 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑥), {𝒫 (𝑔𝑥)}}))) ∈ Comp)
6038, 48, 59kelac2 40601 . . . . . 6 (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}))) ∈ Comp) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅)
6160ex 416 . . . . 5 ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → ((∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔𝑦), {𝒫 (𝑔𝑦)}}))) ∈ Comp → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅))
6236, 61syldc 48 . . . 4 (∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t𝑓) ∈ Comp) → ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅))
6362alrimiv 1935 . . 3 (∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t𝑓) ∈ Comp) → ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅))
64 dfac9 9755 . . 3 (CHOICE ↔ ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅))
6563, 64sylibr 237 . 2 (∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t𝑓) ∈ Comp) → CHOICE)
6620, 65impbii 212 1 (CHOICE ↔ ∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t𝑓) ∈ Comp))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wal 1541   = wceq 1543  wcel 2110  wne 2940  wnel 3046  Vcvv 3413  cin 3870  c0 4242  𝒫 cpw 4518  {csn 4546  {cpr 4548   cuni 4824  cmpt 5140  dom cdm 5556  ran crn 5557  Fun wfun 6379  wf 6381  cfv 6385  Xcixp 8583  cardccrd 9556  CHOICEwac 9734  topGenctg 16947  tcpt 16948  Compccmp 22288  UFLcufl 22802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5184  ax-sep 5197  ax-nul 5204  ax-pow 5263  ax-pr 5327  ax-un 7528
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-pss 3890  df-nul 4243  df-if 4445  df-pw 4520  df-sn 4547  df-pr 4549  df-tp 4551  df-op 4553  df-uni 4825  df-int 4865  df-iun 4911  df-iin 4912  df-br 5059  df-opab 5121  df-mpt 5141  df-tr 5167  df-id 5460  df-eprel 5465  df-po 5473  df-so 5474  df-fr 5514  df-se 5515  df-we 5516  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-pred 6165  df-ord 6221  df-on 6222  df-lim 6223  df-suc 6224  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-fo 6391  df-f1o 6392  df-fv 6393  df-isom 6394  df-riota 7175  df-ov 7221  df-oprab 7222  df-mpo 7223  df-rpss 7516  df-om 7650  df-1st 7766  df-2nd 7767  df-wrecs 8052  df-recs 8113  df-rdg 8151  df-1o 8207  df-oadd 8211  df-omul 8212  df-er 8396  df-map 8515  df-ixp 8584  df-en 8632  df-dom 8633  df-fin 8635  df-fi 9032  df-wdom 9186  df-dju 9522  df-card 9560  df-acn 9563  df-ac 9735  df-topgen 16953  df-pt 16954  df-fbas 20365  df-fg 20366  df-top 21796  df-topon 21813  df-bases 21848  df-cld 21921  df-ntr 21922  df-cls 21923  df-nei 22000  df-cmp 22289  df-fil 22748  df-ufil 22803  df-ufl 22804  df-flim 22841  df-fcls 22843
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator