ttac - Mathbox for Stefan O'Rear

	Mathbox for Stefan O'Rear		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ttac		Structured version Visualization version GIF version

Theorem ttac 42325

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

**Assertion**
Ref	Expression
ttac	⊢ (CHOICE ↔ ∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐))

Proof of Theorem ttac Dummy variable 𝑎 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfac10 10129	. 2 ⊢ (CHOICE ↔ dom card = V)
2		vex 3470	. . . . . 6 ⊢ 𝑐 ∈ V
3		eleq2 2814	. . . . . 6 ⊢ (dom card = V → (𝑐 ∈ dom card ↔ 𝑐 ∈ V))
4	2, 3	mpbiri 258	. . . . 5 ⊢ (dom card = V → 𝑐 ∈ dom card)
5		infxpidm2 10009	. . . . . 6 ⊢ ((𝑐 ∈ dom card ∧ ω ≼ 𝑐) → (𝑐 × 𝑐) ≈ 𝑐)
6	5	ex 412	. . . . 5 ⊢ (𝑐 ∈ dom card → (ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐))
7	4, 6	syl 17	. . . 4 ⊢ (dom card = V → (ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐))
8	7	alrimiv 1922	. . 3 ⊢ (dom card = V → ∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐))
9		finnum 9940	. . . . . . 7 ⊢ (𝑎 ∈ Fin → 𝑎 ∈ dom card)
10	9	adantl 481	. . . . . 6 ⊢ ((∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ 𝑎 ∈ Fin) → 𝑎 ∈ dom card)
11		harcl 9551	. . . . . . . . 9 ⊢ (har‘𝑎) ∈ On
12		onenon 9941	. . . . . . . . 9 ⊢ ((har‘𝑎) ∈ On → (har‘𝑎) ∈ dom card)
13	11, 12	ax-mp 5	. . . . . . . 8 ⊢ (har‘𝑎) ∈ dom card
14		fvex 6895	. . . . . . . . . . . . . 14 ⊢ (har‘𝑎) ∈ V
15		vex 3470	. . . . . . . . . . . . . 14 ⊢ 𝑎 ∈ V
16	14, 15	unex 7727	. . . . . . . . . . . . 13 ⊢ ((har‘𝑎) ∪ 𝑎) ∈ V
17		harinf 42323	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ V ∧ ¬ 𝑎 ∈ Fin) → ω ⊆ (har‘𝑎))
18	15, 17	mpan 687	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑎 ∈ Fin → ω ⊆ (har‘𝑎))
19		ssun1 4165	. . . . . . . . . . . . . 14 ⊢ (har‘𝑎) ⊆ ((har‘𝑎) ∪ 𝑎)
20	18, 19	sstrdi 3987	. . . . . . . . . . . . 13 ⊢ (¬ 𝑎 ∈ Fin → ω ⊆ ((har‘𝑎) ∪ 𝑎))
21		ssdomg 8993	. . . . . . . . . . . . 13 ⊢ (((har‘𝑎) ∪ 𝑎) ∈ V → (ω ⊆ ((har‘𝑎) ∪ 𝑎) → ω ≼ ((har‘𝑎) ∪ 𝑎)))
22	16, 20, 21	mpsyl 68	. . . . . . . . . . . 12 ⊢ (¬ 𝑎 ∈ Fin → ω ≼ ((har‘𝑎) ∪ 𝑎))
23		breq2 5143	. . . . . . . . . . . . . 14 ⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → (ω ≼ 𝑐 ↔ ω ≼ ((har‘𝑎) ∪ 𝑎)))
24		xpeq12 5692	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = ((har‘𝑎) ∪ 𝑎) ∧ 𝑐 = ((har‘𝑎) ∪ 𝑎)) → (𝑐 × 𝑐) = (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)))
25	24	anidms 566	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → (𝑐 × 𝑐) = (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)))
26		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → 𝑐 = ((har‘𝑎) ∪ 𝑎))
27	25, 26	breq12d 5152	. . . . . . . . . . . . . 14 ⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → ((𝑐 × 𝑐) ≈ 𝑐 ↔ (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎)))
28	23, 27	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → ((ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ↔ (ω ≼ ((har‘𝑎) ∪ 𝑎) → (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎))))
29	16, 28	spcv 3587	. . . . . . . . . . . 12 ⊢ (∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) → (ω ≼ ((har‘𝑎) ∪ 𝑎) → (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎)))
30	22, 29	syl5 34	. . . . . . . . . . 11 ⊢ (∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) → (¬ 𝑎 ∈ Fin → (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎)))
31	30	imp 406	. . . . . . . . . 10 ⊢ ((∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ ¬ 𝑎 ∈ Fin) → (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎))
32		harndom 9554	. . . . . . . . . . . 12 ⊢ ¬ (har‘𝑎) ≼ 𝑎
33		ssdomg 8993	. . . . . . . . . . . . . 14 ⊢ (((har‘𝑎) ∪ 𝑎) ∈ V → ((har‘𝑎) ⊆ ((har‘𝑎) ∪ 𝑎) → (har‘𝑎) ≼ ((har‘𝑎) ∪ 𝑎)))
34	16, 19, 33	mp2 9	. . . . . . . . . . . . 13 ⊢ (har‘𝑎) ≼ ((har‘𝑎) ∪ 𝑎)
35		domtr 9000	. . . . . . . . . . . . 13 ⊢ (((har‘𝑎) ≼ ((har‘𝑎) ∪ 𝑎) ∧ ((har‘𝑎) ∪ 𝑎) ≼ 𝑎) → (har‘𝑎) ≼ 𝑎)
36	34, 35	mpan 687	. . . . . . . . . . . 12 ⊢ (((har‘𝑎) ∪ 𝑎) ≼ 𝑎 → (har‘𝑎) ≼ 𝑎)
37	32, 36	mto 196	. . . . . . . . . . 11 ⊢ ¬ ((har‘𝑎) ∪ 𝑎) ≼ 𝑎
38		unxpwdom2 9580	. . . . . . . . . . 11 ⊢ ((((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎) → (((har‘𝑎) ∪ 𝑎) ≼^* (har‘𝑎) ∨ ((har‘𝑎) ∪ 𝑎) ≼ 𝑎))
39		orel2 887	. . . . . . . . . . 11 ⊢ (¬ ((har‘𝑎) ∪ 𝑎) ≼ 𝑎 → ((((har‘𝑎) ∪ 𝑎) ≼^* (har‘𝑎) ∨ ((har‘𝑎) ∪ 𝑎) ≼ 𝑎) → ((har‘𝑎) ∪ 𝑎) ≼^* (har‘𝑎)))
40	37, 38, 39	mpsyl 68	. . . . . . . . . 10 ⊢ ((((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎) → ((har‘𝑎) ∪ 𝑎) ≼^* (har‘𝑎))
41	31, 40	syl 17	. . . . . . . . 9 ⊢ ((∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ ¬ 𝑎 ∈ Fin) → ((har‘𝑎) ∪ 𝑎) ≼^* (har‘𝑎))
42		wdomnumr 10056	. . . . . . . . . 10 ⊢ ((har‘𝑎) ∈ dom card → (((har‘𝑎) ∪ 𝑎) ≼^* (har‘𝑎) ↔ ((har‘𝑎) ∪ 𝑎) ≼ (har‘𝑎)))
43	13, 42	ax-mp 5	. . . . . . . . 9 ⊢ (((har‘𝑎) ∪ 𝑎) ≼^* (har‘𝑎) ↔ ((har‘𝑎) ∪ 𝑎) ≼ (har‘𝑎))
44	41, 43	sylib 217	. . . . . . . 8 ⊢ ((∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ ¬ 𝑎 ∈ Fin) → ((har‘𝑎) ∪ 𝑎) ≼ (har‘𝑎))
45		numdom 10030	. . . . . . . 8 ⊢ (((har‘𝑎) ∈ dom card ∧ ((har‘𝑎) ∪ 𝑎) ≼ (har‘𝑎)) → ((har‘𝑎) ∪ 𝑎) ∈ dom card)
46	13, 44, 45	sylancr 586	. . . . . . 7 ⊢ ((∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ ¬ 𝑎 ∈ Fin) → ((har‘𝑎) ∪ 𝑎) ∈ dom card)
47		ssun2 4166	. . . . . . 7 ⊢ 𝑎 ⊆ ((har‘𝑎) ∪ 𝑎)
48		ssnum 10031	. . . . . . 7 ⊢ ((((har‘𝑎) ∪ 𝑎) ∈ dom card ∧ 𝑎 ⊆ ((har‘𝑎) ∪ 𝑎)) → 𝑎 ∈ dom card)
49	46, 47, 48	sylancl 585	. . . . . 6 ⊢ ((∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ ¬ 𝑎 ∈ Fin) → 𝑎 ∈ dom card)
50	10, 49	pm2.61dan 810	. . . . 5 ⊢ (∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) → 𝑎 ∈ dom card)
51	50	alrimiv 1922	. . . 4 ⊢ (∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) → ∀𝑎 𝑎 ∈ dom card)
52		eqv 3475	. . . 4 ⊢ (dom card = V ↔ ∀𝑎 𝑎 ∈ dom card)
53	51, 52	sylibr 233	. . 3 ⊢ (∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) → dom card = V)
54	8, 53	impbii 208	. 2 ⊢ (dom card = V ↔ ∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐))
55	1, 54	bitri 275	1 ⊢ (CHOICE ↔ ∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 844 ∀wal 1531 = wceq 1533 ∈ wcel 2098 Vcvv 3466 ∪ cun 3939 ⊆ wss 3941 class class class wbr 5139 × cxp 5665 dom cdm 5667 Oncon0 6355 ‘cfv 6534 ωcom 7849 ≈ cen 8933 ≼ cdom 8934 Fincfn 8936 harchar 9548 ≼^* cwdom 9556 cardccrd 9927 CHOICEwac 10107

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-rep 5276 ax-sep 5290 ax-nul 5297 ax-pow 5354 ax-pr 5418 ax-un 7719 ax-inf2 9633

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-ral 3054 df-rex 3063 df-rmo 3368 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3771 df-csb 3887 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-pss 3960 df-nul 4316 df-if 4522 df-pw 4597 df-sn 4622 df-pr 4624 df-op 4628 df-uni 4901 df-int 4942 df-iun 4990 df-br 5140 df-opab 5202 df-mpt 5223 df-tr 5257 df-id 5565 df-eprel 5571 df-po 5579 df-so 5580 df-fr 5622 df-se 5623 df-we 5624 df-xp 5673 df-rel 5674 df-cnv 5675 df-co 5676 df-dm 5677 df-rn 5678 df-res 5679 df-ima 5680 df-pred 6291 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6486 df-fun 6536 df-fn 6537 df-f 6538 df-f1 6539 df-fo 6540 df-f1o 6541 df-fv 6542 df-isom 6543 df-riota 7358 df-ov 7405 df-oprab 7406 df-mpo 7407 df-om 7850 df-1st 7969 df-2nd 7970 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-1o 8462 df-er 8700 df-map 8819 df-en 8937 df-dom 8938 df-sdom 8939 df-fin 8940 df-oi 9502 df-har 9549 df-wdom 9557 df-card 9931 df-acn 9934 df-ac 10108

This theorem is referenced by: (None)

W3C validator