Theorem dfac21 44211

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 3458	. . . . . . 7 ⊢ 𝑓 ∈ V
2	1	dmex 7931	. . . . . 6 ⊢ dom 𝑓 ∈ V
3	2	a1i 11	. . . . 5 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → dom 𝑓 ∈ V)
4		simpr 490	. . . . 5 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → 𝑓:dom 𝑓⟶Comp)
5		fvex 6909	. . . . . . . 8 ⊢ (∏t‘𝑓) ∈ V
6	5	uniex 7768	. . . . . . 7 ⊢ ∪ (∏t‘𝑓) ∈ V
7		acufl 24251	. . . . . . . 8 ⊢ (CHOICE → UFL = V)
8	7	adantr 486	. . . . . . 7 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → UFL = V)
9	6, 8	eleqtrrid 2871	. . . . . 6 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → ∪ (∏t‘𝑓) ∈ UFL)
10		dfac10 10229	. . . . . . . 8 ⊢ (CHOICE ↔ dom card = V)
11	10	birani 509	. . . . . . 7 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → dom card = V)
12	6, 11	eleqtrrid 2871	. . . . . 6 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → ∪ (∏t‘𝑓) ∈ dom card)
13	9, 12	elind 4100	. . . . 5 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → ∪ (∏t‘𝑓) ∈ (UFL ∩ dom card))
14		eqid 2763	. . . . . 6 ⊢ (∏t‘𝑓) = (∏t‘𝑓)
15		eqid 2763	. . . . . 6 ⊢ ∪ (∏t‘𝑓) = ∪ (∏t‘𝑓)
16	14, 15	ptcmpg 24391	. . . . 5 ⊢ ((dom 𝑓 ∈ V ∧ 𝑓:dom 𝑓⟶Comp ∧ ∪ (∏t‘𝑓) ∈ (UFL ∩ dom card)) → (∏t‘𝑓) ∈ Comp)
17	3, 4, 13, 16	syl3anc 1398	. . . 4 ⊢ ((CHOICE ∧ 𝑓:dom 𝑓⟶Comp) → (∏t‘𝑓) ∈ Comp)
18	17	ex 418	. . 3 ⊢ (CHOICE → (𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp))
19	18	alrimiv 1961	. 2 ⊢ (CHOICE → ∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp))
20		fvex 6909	. . . . . . . . 9 ⊢ (𝑔‘𝑦) ∈ V
21		kelac2lem 44209	. . . . . . . . 9 ⊢ ((𝑔‘𝑦) ∈ V → (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}) ∈ Comp)
22	20, 21	mp1i 14	. . . . . . . 8 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑦 ∈ dom 𝑔) → (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}) ∈ Comp)
23	22	fmpttd 7126	. . . . . . 7 ⊢ ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})):dom 𝑔⟶Comp)
24	23	ffdmd 6751	. . . . . 6 ⊢ ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})):dom (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))⟶Comp)
25		vex 3458	. . . . . . . . 9 ⊢ 𝑔 ∈ V
26	25	dmex 7931	. . . . . . . 8 ⊢ dom 𝑔 ∈ V
27	26	mptex 7239	. . . . . . 7 ⊢ (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) ∈ V
28		id 23	. . . . . . . . 9 ⊢ (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) → 𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})))
29		dmeq 5890	. . . . . . . . 9 ⊢ (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) → dom 𝑓 = dom (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})))
30	28, 29	feq12d 6708	. . . . . . . 8 ⊢ (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) → (𝑓:dom 𝑓⟶Comp ↔ (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})):dom (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))⟶Comp))
31		fveq2 6896	. . . . . . . . 9 ⊢ (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) → (∏t‘𝑓) = (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))))
32	31	eleq1d 2849	. . . . . . . 8 ⊢ (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) → ((∏t‘𝑓) ∈ Comp ↔ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp))
33	30, 32	imbi12d 347	. . . . . . 7 ⊢ (𝑓 = (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) → ((𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp) ↔ ((𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})):dom (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))⟶Comp → (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp)))
34	27, 33	spcv 3563	. . . . . 6 ⊢ (∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp) → ((𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})):dom (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))⟶Comp → (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp))
35	24, 34	syl5com 32	. . . . 5 ⊢ ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → (∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp) → (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp))
36		fvex 6909	. . . . . . . 8 ⊢ (𝑔‘𝑥) ∈ V
37	36	a1i 11	. . . . . . 7 ⊢ ((((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ∈ V)
38		df-nel 3066	. . . . . . . . . . 11 ⊢ (∅ ∉ ran 𝑔 ↔ ¬ ∅ ∈ ran 𝑔)
39	38	biimpi 219	. . . . . . . . . 10 ⊢ (∅ ∉ ran 𝑔 → ¬ ∅ ∈ ran 𝑔)
40	39	ad2antlr 740	. . . . . . . . 9 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → ¬ ∅ ∈ ran 𝑔)
41		fvelrn 7087	. . . . . . . . . . . 12 ⊢ ((Fun 𝑔 ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ∈ ran 𝑔)
42	41	adantlr 728	. . . . . . . . . . 11 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ∈ ran 𝑔)
43		eleq1 2852	. . . . . . . . . . 11 ⊢ ((𝑔‘𝑥) = ∅ → ((𝑔‘𝑥) ∈ ran 𝑔 ↔ ∅ ∈ ran 𝑔))
44	42, 43	syl5ibcom 248	. . . . . . . . . 10 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → ((𝑔‘𝑥) = ∅ → ∅ ∈ ran 𝑔))
45	44	necon3bd 2973	. . . . . . . . 9 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → (¬ ∅ ∈ ran 𝑔 → (𝑔‘𝑥) ≠ ∅))
46	40, 45	mpd 16	. . . . . . . 8 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ≠ ∅)
47	46	adantlr 728	. . . . . . 7 ⊢ ((((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp) ∧ 𝑥 ∈ dom 𝑔) → (𝑔‘𝑥) ≠ ∅)
48		fveq2 6896	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → (𝑔‘𝑦) = (𝑔‘𝑥))
49	48	unieqd 4883	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → ∪ (𝑔‘𝑦) = ∪ (𝑔‘𝑥))
50	49	pweqd 4577	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → 𝒫 ∪ (𝑔‘𝑦) = 𝒫 ∪ (𝑔‘𝑥))
51	50	sneqd 4596	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → {𝒫 ∪ (𝑔‘𝑦)} = {𝒫 ∪ (𝑔‘𝑥)})
52	48, 51	preq12d 4702	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → {(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}} = {(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}})
53	52	fveq2d 6900	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}) = (topGen‘{(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}}))
54	53	cbvmptv 5212	. . . . . . . . . 10 ⊢ (𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}})) = (𝑥 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}}))
55	54	fveq2i 6899	. . . . . . . . 9 ⊢ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) = (∏t‘(𝑥 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}})))
56	55	eleq1i 2855	. . . . . . . 8 ⊢ ((∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp ↔ (∏t‘(𝑥 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}}))) ∈ Comp)
57	56	bilani 510	. . . . . . 7 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp) → (∏t‘(𝑥 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑥), {𝒫 ∪ (𝑔‘𝑥)}}))) ∈ Comp)
58	37, 47, 57	kelac2 44210	. . . . . 6 ⊢ (((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) ∧ (∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅)
59	58	ex 418	. . . . 5 ⊢ ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → ((∏t‘(𝑦 ∈ dom 𝑔 ↦ (topGen‘{(𝑔‘𝑦), {𝒫 ∪ (𝑔‘𝑦)}}))) ∈ Comp → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅))
60	35, 59	syldc 49	. . . 4 ⊢ (∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp) → ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅))
61	60	alrimiv 1961	. . 3 ⊢ (∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp) → ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅))
62		dfac9 10228	. . 3 ⊢ (CHOICE ↔ ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔‘𝑥) ≠ ∅))
63	61, 62	sylibr 237	. 2 ⊢ (∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp) → CHOICE)
64	19, 63	impbii 212	1 ⊢ (CHOICE ↔ ∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   = wceq 1569   ∈ wcel 2146   ≠ wne 2959   ∉ wnel 3065  Vcvv 3454   ∩ cin 4092  ∅c0 4281  𝒫 cpw 4560  {csn 4588  {cpr 4590  ∪ cuni 4870   ↦ cmpt 5189  dom cdm 5655  ran crn 5656  Fun wfun 6541  ⟶wf 6543  ‘cfv 6547  Xcixp 8939  cardccrd 10029  CHOICEwac 10207  topGenctg 17623  ∏_tcpt 17624  Compccmp 23719  UFLcufl 24234

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7761

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6311  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6501  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-isom 6556  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-rpss 7749  df-om 7888  df-1st 8011  df-2nd 8012  df-frecs 8313  df-wrecs 8344  df-recs 8393  df-rdg 8432  df-1o 8490  df-2o 8491  df-oadd 8494  df-omul 8495  df-er 8731  df-map 8863  df-ixp 8940  df-en 8988  df-dom 8989  df-fin 8991  df-fi 9416  df-wdom 9572  df-dju 9995  df-card 10033  df-acn 10036  df-ac 10208  df-topgen 17629  df-pt 17630  df-fbas 21690  df-fg 21691  df-top 23227  df-topon 23244  df-bases 23279  df-cld 23352  df-ntr 23353  df-cls 23354  df-nei 23431  df-cmp 23720  df-fil 24180  df-ufil 24235  df-ufl 24236  df-flim 24273  df-fcls 24275

This theorem is used by: (None)