Theorem dfac21 43090

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 3463	. . . . . . 7 ⊢ 𝑓 ∈ V
2	1	dmex 7905	. . . . . 6 ⊢ dom 𝑓 ∈ V
3	2	a1i 11	. . . . 5 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → dom 𝑓 ∈ V)
4		simpr 484	. . . . 5 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → 𝑓:dom 𝑓⟶Comp)
5		fvex 6889	. . . . . . . 8 ⊢ (∏t‘𝑓) ∈ V
6	5	uniex 7735	. . . . . . 7 ⊢ ∪ (∏t‘𝑓) ∈ V
7		acufl 23855	. . . . . . . 8 ⊢ (CHOICE → UFL = V)
8	7	adantr 480	. . . . . . 7 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → UFL = V)
9	6, 8	eleqtrrid 2841	. . . . . 6 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → ∪ (∏t‘𝑓) ∈ UFL)
10		simpl 482	. . . . . . . 8 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → CHOICE)
11		dfac10 10152	. . . . . . . 8 ⊢ (CHOICE ↔ dom card = V)
12	10, 11	sylib 218	. . . . . . 7 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → dom card = V)
13	6, 12	eleqtrrid 2841	. . . . . 6 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → ∪ (∏t‘𝑓) ∈ dom card)
14	9, 13	elind 4175	. . . . 5 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → ∪ (∏t‘𝑓) ∈ (UFL ∩ dom card))
15		eqid 2735	. . . . . 6 ⊢ (∏t‘𝑓) = (∏t‘𝑓)
16		eqid 2735	. . . . . 6 ⊢ ∪ (∏t‘𝑓) = ∪ (∏t‘𝑓)
17	15, 16	ptcmpg 23995	. . . . 5 ⊢ ((dom 𝑓 ∈ V ∧ 𝑓:dom 𝑓⟶Comp ∧ ∪ (∏t‘𝑓) ∈ (UFL ∩ dom card)) → (∏t‘𝑓) ∈ Comp)
18	3, 4, 14, 17	syl3anc 1373	. . . 4 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → (∏t‘𝑓) ∈ Comp)
19	18	ex 412	. . 3 ⊢ (CHOICE → (𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp))
20	19	alrimiv 1927	. 2 ⊢ (CHOICE → ∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp))
21		fvex 6889	. . . . . . . . 9 ⊢ (𝑔‘𝑦) ∈ V
22		kelac2lem 43088	. . . . . . . . 9 ⊢ ((𝑔‘𝑦) ∈ V → (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}) ∈ Comp)
23	21, 22	mp1i 13	. . . . . . . 8 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑦 ∈ dom 𝑔) → (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}) ∈ Comp)
24	23	fmpttd 7105	. . . . . . 7 ⊢ ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})):dom 𝑔⟶Comp)
25	24	ffdmd 6736	. . . . . 6 ⊢ ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})):dom (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))⟶Comp)
26		vex 3463	. . . . . . . . 9 ⊢ 𝑔 ∈ V
27	26	dmex 7905	. . . . . . . 8 ⊢ dom 𝑔 ∈ V
28	27	mptex 7215	. . . . . . 7 ⊢ (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) ∈ V
29		id 22	. . . . . . . . 9 ⊢ (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) → 𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})))
30		dmeq 5883	. . . . . . . . 9 ⊢ (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) → dom 𝑓 = dom (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})))
31	29, 30	feq12d 6694	. . . . . . . 8 ⊢ (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) → (𝑓:dom 𝑓⟶Comp ↔ (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})):dom (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))⟶Comp))
32		fveq2 6876	. . . . . . . . 9 ⊢ (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) → (∏t‘𝑓) = (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))))
33	32	eleq1d 2819	. . . . . . . 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 3584	. . . . . 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 6889	. . . . . . . 8 ⊢ (𝑔‘𝑥) ∈ V
38	37	a1i 11	. . . . . . 7 ⊢ ((((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ∈ V)
39		df-nel 3037	. . . . . . . . . . 11 ⊢ (∅ ∉ ran 𝑔 ↔ ¬ ∅ ∈ ran 𝑔)
40	39	biimpi 216	. . . . . . . . . 10 ⊢ (∅ ∉ ran 𝑔 → ¬ ∅ ∈ ran 𝑔)
41	40	ad2antlr 727	. . . . . . . . 9 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → ¬ ∅ ∈ ran 𝑔)
42		fvelrn 7066	. . . . . . . . . . . 12 ⊢ ((Fun 𝑔 ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ∈ ran 𝑔)
43	42	adantlr 715	. . . . . . . . . . 11 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ∈ ran 𝑔)
44		eleq1 2822	. . . . . . . . . . 11 ⊢ ((𝑔‘𝑥) = ∅ → ((𝑔‘𝑥) ∈ ran 𝑔 ↔ ∅ ∈ ran 𝑔))
45	43, 44	syl5ibcom 245	. . . . . . . . . 10 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → ((𝑔‘𝑥) = ∅ → ∅ ∈ ran 𝑔))
46	45	necon3bd 2946	. . . . . . . . 9 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → (¬ ∅ ∈ ran 𝑔 → (𝑔‘𝑥) ≠ ∅))
47	41, 46	mpd 15	. . . . . . . 8 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ≠ ∅)
48	47	adantlr 715	. . . . . . 7 ⊢ ((((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ≠ ∅)
49		fveq2 6876	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (𝑔‘𝑦) = (𝑔‘𝑥))
50	49	unieqd 4896	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → ∪ (𝑔‘𝑦) = ∪ (𝑔‘𝑥))
51	50	pweqd 4592	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → 𝒫 ∪ (𝑔‘𝑦) = 𝒫 ∪ (𝑔‘𝑥))
52	51	sneqd 4613	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → {𝒫 ∪ (𝑔‘𝑦)} = {𝒫 ∪ (𝑔‘𝑥)})
53	49, 52	preq12d 4717	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → {(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}} = {(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}})
54	53	fveq2d 6880	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}) = (topGen‘{(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}}))
55	54	cbvmptv 5225	. . . . . . . . . . 11 ⊢ (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) = (𝑥 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}}))
56	55	fveq2i 6879	. . . . . . . . . 10 ⊢ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) = (∏t‘(𝑥 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}})))
57	56	eleq1i 2825	. . . . . . . . 9 ⊢ ((∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp ↔ (∏t‘(𝑥 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}}))) ∈ Comp)
58	57	biimpi 216	. . . . . . . 8 ⊢ ((∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp → (∏t‘(𝑥 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}}))) ∈ Comp)
59	58	adantl 481	. . . . . . 7 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp) → (∏t‘(𝑥 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}}))) ∈ Comp)
60	38, 48, 59	kelac2 43089	. . . . . 6 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅)
61	60	ex 412	. . . . 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 1927	. . 3 ⊢ (∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp) → ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅))
64		dfac9 10151	. . 3 ⊢ (CHOICE ↔ ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅))
65	63, 64	sylibr 234	. 2 ⊢ (∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp) → CHOICE)
66	20, 65	impbii 209	1 ⊢ (CHOICE ↔ ∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540   ∈ wcel 2108   ≠ wne 2932   ∉ wnel 3036  Vcvv 3459   ∩ cin 3925  ∅c0 4308  𝒫 cpw 4575  {csn 4601  {cpr 4603  ∪ cuni 4883   ↦ cmpt 5201  dom cdm 5654  ran crn 5655  Fun wfun 6525  ⟶wf 6527  ‘cfv 6531  Xcixp 8911  cardccrd 9949  CHOICEwac 10129  topGenctg 17451  ∏_tcpt 17452  Compccmp 23324  UFLcufl 23838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-int 4923  df-iun 4969  df-iin 4970  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-se 5607  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-isom 6540  df-riota 7362  df-ov 7408  df-oprab 7409  df-mpo 7410  df-rpss 7717  df-om 7862  df-1st 7988  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-oadd 8484  df-omul 8485  df-er 8719  df-map 8842  df-ixp 8912  df-en 8960  df-dom 8961  df-fin 8963  df-fi 9423  df-wdom 9579  df-dju 9915  df-card 9953  df-acn 9956  df-ac 10130  df-topgen 17457  df-pt 17458  df-fbas 21312  df-fg 21313  df-top 22832  df-topon 22849  df-bases 22884  df-cld 22957  df-ntr 22958  df-cls 22959  df-nei 23036  df-cmp 23325  df-fil 23784  df-ufil 23839  df-ufl 23840  df-flim 23877  df-fcls 23879

This theorem is referenced by: (None)