Metamath Proof Explorer

Theorem ttac

Description: Tarski's theorem about choice: infxpidm is equivalent to ax-ac . (Contributed by Stefan O'Rear, 4-Nov-2014) (Proof shortened by Stefan O'Rear, 10-Jul-2015)

Ref Expression
Assertion ttac ⊢ CHOICE ↔ ∀ c ω ≼ c → c × c ≈ c

Proof

Step Hyp Ref Expression
1 dfac10 ⊢ CHOICE ↔ dom ⁡ card = V
2 vex ⊢ c ∈ V
3 eleq2 ⊢ dom ⁡ card = V → c ∈ dom ⁡ card ↔ c ∈ V
4 2 3 mpbiri ⊢ dom ⁡ card = V → c ∈ dom ⁡ card
5 infxpidm2 ⊢ c ∈ dom ⁡ card ∧ ω ≼ c → c × c ≈ c
6 5 ex ⊢ c ∈ dom ⁡ card → ω ≼ c → c × c ≈ c
7 4 6 syl ⊢ dom ⁡ card = V → ω ≼ c → c × c ≈ c
8 7 alrimiv ⊢ dom ⁡ card = V → ∀ c ω ≼ c → c × c ≈ c
9 finnum ⊢ a ∈ Fin → a ∈ dom ⁡ card
10 9 adantl ⊢ ∀ c ω ≼ c → c × c ≈ c ∧ a ∈ Fin → a ∈ dom ⁡ card
11 harcl ⊢ har ⁡ a ∈ On
12 onenon ⊢ har ⁡ a ∈ On → har ⁡ a ∈ dom ⁡ card
13 11 12 ax-mp ⊢ har ⁡ a ∈ dom ⁡ card
14 fvex ⊢ har ⁡ a ∈ V
15 vex ⊢ a ∈ V
16 14 15 unex ⊢ har ⁡ a ∪ a ∈ V
17 harinf ⊢ a ∈ V ∧ ¬ a ∈ Fin → ω ⊆ har ⁡ a
18 15 17 mpan ⊢ ¬ a ∈ Fin → ω ⊆ har ⁡ a
19 ssun1 ⊢ har ⁡ a ⊆ har ⁡ a ∪ a
20 18 19 sstrdi ⊢ ¬ a ∈ Fin → ω ⊆ har ⁡ a ∪ a
21 ssdomg ⊢ har ⁡ a ∪ a ∈ V → ω ⊆ har ⁡ a ∪ a → ω ≼ har ⁡ a ∪ a
22 16 20 21 mpsyl ⊢ ¬ a ∈ Fin → ω ≼ har ⁡ a ∪ a
23 breq2 ⊢ c = har ⁡ a ∪ a → ω ≼ c ↔ ω ≼ har ⁡ a ∪ a
24 xpeq12 ⊢ c = har ⁡ a ∪ a ∧ c = har ⁡ a ∪ a → c × c = har ⁡ a ∪ a × har ⁡ a ∪ a
25 24 anidms ⊢ c = har ⁡ a ∪ a → c × c = har ⁡ a ∪ a × har ⁡ a ∪ a
26 id ⊢ c = har ⁡ a ∪ a → c = har ⁡ a ∪ a
27 25 26 breq12d ⊢ c = har ⁡ a ∪ a → c × c ≈ c ↔ har ⁡ a ∪ a × har ⁡ a ∪ a ≈ har ⁡ a ∪ a
28 23 27 imbi12d ⊢ c = har ⁡ a ∪ a → ω ≼ c → c × c ≈ c ↔ ω ≼ har ⁡ a ∪ a → har ⁡ a ∪ a × har ⁡ a ∪ a ≈ har ⁡ a ∪ a
29 16 28 spcv ⊢ ∀ c ω ≼ c → c × c ≈ c → ω ≼ har ⁡ a ∪ a → har ⁡ a ∪ a × har ⁡ a ∪ a ≈ har ⁡ a ∪ a
30 22 29 syl5 ⊢ ∀ c ω ≼ c → c × c ≈ c → ¬ a ∈ Fin → har ⁡ a ∪ a × har ⁡ a ∪ a ≈ har ⁡ a ∪ a
31 30 imp ⊢ ∀ c ω ≼ c → c × c ≈ c ∧ ¬ a ∈ Fin → har ⁡ a ∪ a × har ⁡ a ∪ a ≈ har ⁡ a ∪ a
32 harndom ⊢ ¬ har ⁡ a ≼ a
33 ssdomg ⊢ har ⁡ a ∪ a ∈ V → har ⁡ a ⊆ har ⁡ a ∪ a → har ⁡ a ≼ har ⁡ a ∪ a
34 16 19 33 mp2 ⊢ har ⁡ a ≼ har ⁡ a ∪ a
35 domtr ⊢ har ⁡ a ≼ har ⁡ a ∪ a ∧ har ⁡ a ∪ a ≼ a → har ⁡ a ≼ a
36 34 35 mpan ⊢ har ⁡ a ∪ a ≼ a → har ⁡ a ≼ a
37 32 36 mto ⊢ ¬ har ⁡ a ∪ a ≼ a
38 unxpwdom2 ⊢ har ⁡ a ∪ a × har ⁡ a ∪ a ≈ har ⁡ a ∪ a → har ⁡ a ∪ a ≼ * har ⁡ a ∨ har ⁡ a ∪ a ≼ a
39 orel2 ⊢ ¬ har ⁡ a ∪ a ≼ a → har ⁡ a ∪ a ≼ * har ⁡ a ∨ har ⁡ a ∪ a ≼ a → har ⁡ a ∪ a ≼ * har ⁡ a
40 37 38 39 mpsyl ⊢ har ⁡ a ∪ a × har ⁡ a ∪ a ≈ har ⁡ a ∪ a → har ⁡ a ∪ a ≼ * har ⁡ a
41 31 40 syl ⊢ ∀ c ω ≼ c → c × c ≈ c ∧ ¬ a ∈ Fin → har ⁡ a ∪ a ≼ * har ⁡ a
42 wdomnumr ⊢ har ⁡ a ∈ dom ⁡ card → har ⁡ a ∪ a ≼ * har ⁡ a ↔ har ⁡ a ∪ a ≼ har ⁡ a
43 13 42 ax-mp ⊢ har ⁡ a ∪ a ≼ * har ⁡ a ↔ har ⁡ a ∪ a ≼ har ⁡ a
44 41 43 sylib ⊢ ∀ c ω ≼ c → c × c ≈ c ∧ ¬ a ∈ Fin → har ⁡ a ∪ a ≼ har ⁡ a
45 numdom ⊢ har ⁡ a ∈ dom ⁡ card ∧ har ⁡ a ∪ a ≼ har ⁡ a → har ⁡ a ∪ a ∈ dom ⁡ card
46 13 44 45 sylancr ⊢ ∀ c ω ≼ c → c × c ≈ c ∧ ¬ a ∈ Fin → har ⁡ a ∪ a ∈ dom ⁡ card
47 ssun2 ⊢ a ⊆ har ⁡ a ∪ a
48 ssnum ⊢ har ⁡ a ∪ a ∈ dom ⁡ card ∧ a ⊆ har ⁡ a ∪ a → a ∈ dom ⁡ card
49 46 47 48 sylancl ⊢ ∀ c ω ≼ c → c × c ≈ c ∧ ¬ a ∈ Fin → a ∈ dom ⁡ card
50 10 49 pm2.61dan ⊢ ∀ c ω ≼ c → c × c ≈ c → a ∈ dom ⁡ card
51 50 alrimiv ⊢ ∀ c ω ≼ c → c × c ≈ c → ∀ a a ∈ dom ⁡ card
52 eqv ⊢ dom ⁡ card = V ↔ ∀ a a ∈ dom ⁡ card
53 51 52 sylibr ⊢ ∀ c ω ≼ c → c × c ≈ c → dom ⁡ card = V
54 8 53 impbii ⊢ dom ⁡ card = V ↔ ∀ c ω ≼ c → c × c ≈ c
55 1 54 bitri ⊢ CHOICE ↔ ∀ c ω ≼ c → c × c ≈ c