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