Theorem dfac21 41451

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.

Step	Hyp	Ref	Expression
1		vex 3450	. . . . . . 7 ⊢ 𝑓 ∈ V
2	1	dmex 7853	. . . . . 6 ⊢ dom 𝑓 ∈ V
3	2	a1i 11	. . . . 5 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → dom 𝑓 ∈ V)
4		simpr 485	. . . . 5 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → 𝑓:dom 𝑓⟶Comp)
5		fvex 6860	. . . . . . . 8 ⊢ (∏t‘𝑓) ∈ V
6	5	uniex 7683	. . . . . . 7 ⊢ ∪ (∏t‘𝑓) ∈ V
7		acufl 23305	. . . . . . . 8 ⊢ (CHOICE → UFL = V)
8	7	adantr 481	. . . . . . 7 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → UFL = V)
9	6, 8	eleqtrrid 2839	. . . . . 6 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → ∪ (∏t‘𝑓) ∈ UFL)
10		simpl 483	. . . . . . . 8 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → CHOICE)
11		dfac10 10082	. . . . . . . 8 ⊢ (CHOICE ↔ dom card = V)
12	10, 11	sylib 217	. . . . . . 7 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → dom card = V)
13	6, 12	eleqtrrid 2839	. . . . . 6 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → ∪ (∏t‘𝑓) ∈ dom card)
14	9, 13	elind 4159	. . . . 5 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → ∪ (∏t‘𝑓) ∈ (UFL ∩ dom card))
15		eqid 2731	. . . . . 6 ⊢ (∏t‘𝑓) = (∏t‘𝑓)
16		eqid 2731	. . . . . 6 ⊢ ∪ (∏t‘𝑓) = ∪ (∏t‘𝑓)
17	15, 16	ptcmpg 23445	. . . . 5 ⊢ ((dom 𝑓 ∈ V ∧ 𝑓:dom 𝑓⟶Comp ∧ ∪ (∏t‘𝑓) ∈ (UFL ∩ dom card)) → (∏t‘𝑓) ∈ Comp)
18	3, 4, 14, 17	syl3anc 1371	. . . 4 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → (∏t‘𝑓) ∈ Comp)
19	18	ex 413	. . 3 ⊢ (CHOICE → (𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp))
20	19	alrimiv 1930	. 2 ⊢ (CHOICE → ∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp))
21		fvex 6860	. . . . . . . . 9 ⊢ (𝑔‘𝑦) ∈ V
22		kelac2lem 41449	. . . . . . . . 9 ⊢ ((𝑔‘𝑦) ∈ V → (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}) ∈ Comp)
23	21, 22	mp1i 13	. . . . . . . 8 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑦 ∈ dom 𝑔) → (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}) ∈ Comp)
24	23	fmpttd 7068	. . . . . . 7 ⊢ ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})):dom 𝑔⟶Comp)
25	24	ffdmd 6704	. . . . . 6 ⊢ ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})):dom (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))⟶Comp)
26		vex 3450	. . . . . . . . 9 ⊢ 𝑔 ∈ V
27	26	dmex 7853	. . . . . . . 8 ⊢ dom 𝑔 ∈ V
28	27	mptex 7178	. . . . . . 7 ⊢ (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) ∈ V
29		id 22	. . . . . . . . 9 ⊢ (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) → 𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})))
30		dmeq 5864	. . . . . . . . 9 ⊢ (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) → dom 𝑓 = dom (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})))
31	29, 30	feq12d 6661	. . . . . . . 8 ⊢ (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) → (𝑓:dom 𝑓⟶Comp ↔ (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})):dom (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))⟶Comp))
32		fveq2 6847	. . . . . . . . 9 ⊢ (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) → (∏t‘𝑓) = (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))))
33	32	eleq1d 2817	. . . . . . . 8 ⊢ (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) → ((∏t‘𝑓) ∈ Comp ↔ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp))
34	31, 33	imbi12d 344	. . . . . . 7 ⊢ (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) → ((𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp) ↔ ((𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})):dom (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))⟶Comp → (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp)))
35	28, 34	spcv 3565	. . . . . 6 ⊢ (∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp) → ((𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})):dom (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))⟶Comp → (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp))
36	25, 35	syl5com 31	. . . . 5 ⊢ ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → (∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp) → (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp))
37		fvex 6860	. . . . . . . 8 ⊢ (𝑔‘𝑥) ∈ V
38	37	a1i 11	. . . . . . 7 ⊢ ((((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ∈ V)
39		df-nel 3046	. . . . . . . . . . 11 ⊢ (∅ ∉ ran 𝑔 ↔ ¬ ∅ ∈ ran 𝑔)
40	39	biimpi 215	. . . . . . . . . 10 ⊢ (∅ ∉ ran 𝑔 → ¬ ∅ ∈ ran 𝑔)
41	40	ad2antlr 725	. . . . . . . . 9 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → ¬ ∅ ∈ ran 𝑔)
42		fvelrn 7032	. . . . . . . . . . . 12 ⊢ ((Fun 𝑔 ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ∈ ran 𝑔)
43	42	adantlr 713	. . . . . . . . . . 11 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ∈ ran 𝑔)
44		eleq1 2820	. . . . . . . . . . 11 ⊢ ((𝑔‘𝑥) = ∅ → ((𝑔‘𝑥) ∈ ran 𝑔 ↔ ∅ ∈ ran 𝑔))
45	43, 44	syl5ibcom 244	. . . . . . . . . 10 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → ((𝑔‘𝑥) = ∅ → ∅ ∈ ran 𝑔))
46	45	necon3bd 2953	. . . . . . . . 9 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → (¬ ∅ ∈ ran 𝑔 → (𝑔‘𝑥) ≠ ∅))
47	41, 46	mpd 15	. . . . . . . 8 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ≠ ∅)
48	47	adantlr 713	. . . . . . 7 ⊢ ((((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ≠ ∅)
49		fveq2 6847	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (𝑔‘𝑦) = (𝑔‘𝑥))
50	49	unieqd 4884	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → ∪ (𝑔‘𝑦) = ∪ (𝑔‘𝑥))
51	50	pweqd 4582	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → 𝒫 ∪ (𝑔‘𝑦) = 𝒫 ∪ (𝑔‘𝑥))
52	51	sneqd 4603	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → {𝒫 ∪ (𝑔‘𝑦)} = {𝒫 ∪ (𝑔‘𝑥)})
53	49, 52	preq12d 4707	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → {(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}} = {(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}})
54	53	fveq2d 6851	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}) = (topGen‘{(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}}))
55	54	cbvmptv 5223	. . . . . . . . . . 11 ⊢ (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) = (𝑥 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}}))
56	55	fveq2i 6850	. . . . . . . . . 10 ⊢ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) = (∏t‘(𝑥 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}})))
57	56	eleq1i 2823	. . . . . . . . 9 ⊢ ((∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp ↔ (∏t‘(𝑥 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}}))) ∈ Comp)
58	57	biimpi 215	. . . . . . . 8 ⊢ ((∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp → (∏t‘(𝑥 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}}))) ∈ Comp)
59	58	adantl 482	. . . . . . 7 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp) → (∏t‘(𝑥 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}}))) ∈ Comp)
60	38, 48, 59	kelac2 41450	. . . . . 6 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅)
61	60	ex 413	. . . . 5 ⊢ ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → ((∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅))
62	36, 61	syldc 48	. . . 4 ⊢ (∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp) → ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅))
63	62	alrimiv 1930	. . 3 ⊢ (∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp) → ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅))
64		dfac9 10081	. . 3 ⊢ (CHOICE ↔ ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅))
65	63, 64	sylibr 233	. 2 ⊢ (∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp) → CHOICE)
66	20, 65	impbii 208	1 ⊢ (CHOICE ↔ ∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1539   = wceq 1541   ∈ wcel 2106   ≠ wne 2939   ∉ wnel 3045  Vcvv 3446   ∩ cin 3912  ∅c0 4287  𝒫 cpw 4565  {csn 4591  {cpr 4593  ∪ cuni 4870   ↦ cmpt 5193  dom cdm 5638  ran crn 5639  Fun wfun 6495  ⟶wf 6497  ‘cfv 6501  Xcixp 8842  cardccrd 9880  CHOICEwac 10060  topGenctg 17333  ∏_tcpt 17334  Compccmp 22774  UFLcufl 23288

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 2702  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677

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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-rpss 7665  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-oadd 8421  df-omul 8422  df-er 8655  df-map 8774  df-ixp 8843  df-en 8891  df-dom 8892  df-fin 8894  df-fi 9356  df-wdom 9510  df-dju 9846  df-card 9884  df-acn 9887  df-ac 10061  df-topgen 17339  df-pt 17340  df-fbas 20830  df-fg 20831  df-top 22280  df-topon 22297  df-bases 22333  df-cld 22407  df-ntr 22408  df-cls 22409  df-nei 22486  df-cmp 22775  df-fil 23234  df-ufil 23289  df-ufl 23290  df-flim 23327  df-fcls 23329

This theorem is referenced by: (None)