Metamath Proof Explorer

Theorem dfac21

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)

Ref Expression
Assertion dfac21 ( CHOICE ↔ ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Comp → ( ∏t ‘ 𝑓 ) ∈ Comp ) )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑓 ∈ V
2 1 dmex ⊢ dom 𝑓 ∈ V
3 2 a1i ⊢ ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Comp ) → dom 𝑓 ∈ V )
4 simpr ⊢ ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Comp ) → 𝑓 : dom 𝑓 ⟶ Comp )
5 fvex ⊢ ( ∏t ‘ 𝑓 ) ∈ V
6 5 uniex ⊢ ∪ ( ∏t ‘ 𝑓 ) ∈ V
7 acufl ⊢ ( CHOICE → UFL = V )
8 7 adantr ⊢ ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Comp ) → UFL = V )
9 6 8 eleqtrrid ⊢ ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Comp ) → ∪ ( ∏t ‘ 𝑓 ) ∈ UFL )
10 simpl ⊢ ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Comp ) → CHOICE )
11 dfac10 ⊢ ( CHOICE ↔ dom card = V )
12 10 11 sylib ⊢ ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Comp ) → dom card = V )
13 6 12 eleqtrrid ⊢ ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Comp ) → ∪ ( ∏t ‘ 𝑓 ) ∈ dom card )
14 9 13 elind ⊢ ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Comp ) → ∪ ( ∏t ‘ 𝑓 ) ∈ ( UFL ∩ dom card ) )
15 eqid ⊢ ( ∏t ‘ 𝑓 ) = ( ∏t ‘ 𝑓 )
16 eqid ⊢ ∪ ( ∏t ‘ 𝑓 ) = ∪ ( ∏t ‘ 𝑓 )
17 15 16 ptcmpg ⊢ ( ( dom 𝑓 ∈ V ∧ 𝑓 : dom 𝑓 ⟶ Comp ∧ ∪ ( ∏t ‘ 𝑓 ) ∈ ( UFL ∩ dom card ) ) → ( ∏t ‘ 𝑓 ) ∈ Comp )
18 3 4 14 17 syl3anc ⊢ ( ( CHOICE ∧ 𝑓 : dom 𝑓 ⟶ Comp ) → ( ∏t ‘ 𝑓 ) ∈ Comp )
19 18 ex ⊢ ( CHOICE → ( 𝑓 : dom 𝑓 ⟶ Comp → ( ∏t ‘ 𝑓 ) ∈ Comp ) )
20 19 alrimiv ⊢ ( CHOICE → ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Comp → ( ∏t ‘ 𝑓 ) ∈ Comp ) )
21 fvex ⊢ ( 𝑔 ‘ 𝑦 ) ∈ V
22 kelac2lem ⊢ ( ( 𝑔 ‘ 𝑦 ) ∈ V → ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ∈ Comp )
23 21 22 mp1i ⊢ ( ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ∧ 𝑦 ∈ dom 𝑔 ) → ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ∈ Comp )
24 23 fmpttd ⊢ ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) → ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) : dom 𝑔 ⟶ Comp )
25 24 ffdmd ⊢ ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) → ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) : dom ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) ⟶ Comp )
26 vex ⊢ 𝑔 ∈ V
27 26 dmex ⊢ dom 𝑔 ∈ V
28 27 mptex ⊢ ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) ∈ V
29 id ⊢ ( 𝑓 = ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) → 𝑓 = ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) )
30 dmeq ⊢ ( 𝑓 = ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) → dom 𝑓 = dom ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) )
31 29 30 feq12d ⊢ ( 𝑓 = ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) → ( 𝑓 : dom 𝑓 ⟶ Comp ↔ ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) : dom ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) ⟶ Comp ) )
32 fveq2 ⊢ ( 𝑓 = ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) → ( ∏t ‘ 𝑓 ) = ( ∏t ‘ ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) ) )
33 32 eleq1d ⊢ ( 𝑓 = ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) → ( ( ∏t ‘ 𝑓 ) ∈ Comp ↔ ( ∏t ‘ ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) ) ∈ Comp ) )
34 31 33 imbi12d ⊢ ( 𝑓 = ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) → ( ( 𝑓 : dom 𝑓 ⟶ Comp → ( ∏t ‘ 𝑓 ) ∈ Comp ) ↔ ( ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) : dom ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) ⟶ Comp → ( ∏t ‘ ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) ) ∈ Comp ) ) )
35 28 34 spcv ⊢ ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Comp → ( ∏t ‘ 𝑓 ) ∈ Comp ) → ( ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) : dom ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) ⟶ Comp → ( ∏t ‘ ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) ) ∈ Comp ) )
36 25 35 syl5com ⊢ ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) → ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Comp → ( ∏t ‘ 𝑓 ) ∈ Comp ) → ( ∏t ‘ ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) ) ∈ Comp ) )
37 fvex ⊢ ( 𝑔 ‘ 𝑥 ) ∈ V
38 37 a1i ⊢ ( ( ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ∧ ( ∏t ‘ ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) ) ∈ Comp ) ∧ 𝑥 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑥 ) ∈ V )
39 df-nel ⊢ ( ∅ ∉ ran 𝑔 ↔ ¬ ∅ ∈ ran 𝑔 )
40 39 biimpi ⊢ ( ∅ ∉ ran 𝑔 → ¬ ∅ ∈ ran 𝑔 )
41 40 ad2antlr ⊢ ( ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ∧ 𝑥 ∈ dom 𝑔 ) → ¬ ∅ ∈ ran 𝑔 )
42 fvelrn ⊢ ( ( Fun 𝑔 ∧ 𝑥 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑥 ) ∈ ran 𝑔 )
43 42 adantlr ⊢ ( ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ∧ 𝑥 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑥 ) ∈ ran 𝑔 )
44 eleq1 ⊢ ( ( 𝑔 ‘ 𝑥 ) = ∅ → ( ( 𝑔 ‘ 𝑥 ) ∈ ran 𝑔 ↔ ∅ ∈ ran 𝑔 ) )
45 43 44 syl5ibcom ⊢ ( ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ∧ 𝑥 ∈ dom 𝑔 ) → ( ( 𝑔 ‘ 𝑥 ) = ∅ → ∅ ∈ ran 𝑔 ) )
46 45 necon3bd ⊢ ( ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ∧ 𝑥 ∈ dom 𝑔 ) → ( ¬ ∅ ∈ ran 𝑔 → ( 𝑔 ‘ 𝑥 ) ≠ ∅ ) )
47 41 46 mpd ⊢ ( ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ∧ 𝑥 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑥 ) ≠ ∅ )
48 47 adantlr ⊢ ( ( ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ∧ ( ∏t ‘ ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) ) ∈ Comp ) ∧ 𝑥 ∈ dom 𝑔 ) → ( 𝑔 ‘ 𝑥 ) ≠ ∅ )
49 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑔 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑥 ) )
50 49 unieqd ⊢ ( 𝑦 = 𝑥 → ∪ ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑔 ‘ 𝑥 ) )
51 50 pweqd ⊢ ( 𝑦 = 𝑥 → 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) = 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) )
52 51 sneqd ⊢ ( 𝑦 = 𝑥 → { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } = { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } )
53 49 52 preq12d ⊢ ( 𝑦 = 𝑥 → { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } = { ( 𝑔 ‘ 𝑥 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } } )
54 53 fveq2d ⊢ ( 𝑦 = 𝑥 → ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) = ( topGen ‘ { ( 𝑔 ‘ 𝑥 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } } ) )
55 54 cbvmptv ⊢ ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) = ( 𝑥 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑥 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } } ) )
56 55 fveq2i ⊢ ( ∏t ‘ ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) ) = ( ∏t ‘ ( 𝑥 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑥 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } } ) ) )
57 56 eleq1i ⊢ ( ( ∏t ‘ ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) ) ∈ Comp ↔ ( ∏t ‘ ( 𝑥 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑥 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } } ) ) ) ∈ Comp )
58 57 biimpi ⊢ ( ( ∏t ‘ ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) ) ∈ Comp → ( ∏t ‘ ( 𝑥 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑥 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } } ) ) ) ∈ Comp )
59 58 adantl ⊢ ( ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ∧ ( ∏t ‘ ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) ) ∈ Comp ) → ( ∏t ‘ ( 𝑥 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑥 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑥 ) } } ) ) ) ∈ Comp )
60 38 48 59 kelac2 ⊢ ( ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) ∧ ( ∏t ‘ ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) ) ∈ Comp ) → X 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) ≠ ∅ )
61 60 ex ⊢ ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) → ( ( ∏t ‘ ( 𝑦 ∈ dom 𝑔 ↦ ( topGen ‘ { ( 𝑔 ‘ 𝑦 ) , { 𝒫 ∪ ( 𝑔 ‘ 𝑦 ) } } ) ) ) ∈ Comp → X 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) ≠ ∅ ) )
62 36 61 syldc ⊢ ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Comp → ( ∏t ‘ 𝑓 ) ∈ Comp ) → ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) → X 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) ≠ ∅ ) )
63 62 alrimiv ⊢ ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Comp → ( ∏t ‘ 𝑓 ) ∈ Comp ) → ∀ 𝑔 ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) → X 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) ≠ ∅ ) )
64 dfac9 ⊢ ( CHOICE ↔ ∀ 𝑔 ( ( Fun 𝑔 ∧ ∅ ∉ ran 𝑔 ) → X 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) ≠ ∅ ) )
65 63 64 sylibr ⊢ ( ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Comp → ( ∏t ‘ 𝑓 ) ∈ Comp ) → CHOICE )
66 20 65 impbii ⊢ ( CHOICE ↔ ∀ 𝑓 ( 𝑓 : dom 𝑓 ⟶ Comp → ( ∏t ‘ 𝑓 ) ∈ Comp ) )