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 42451

Description: Tarski's theorem about choice: infxpidm 10579 is equivalent to ax-ac 10476. (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 10154	. 2 ⊢ (CHOICE ↔ dom card = V)
2		vex 3474	. . . . . 6 ⊢ 𝑐 ∈ V
3		eleq2 2818	. . . . . 6 ⊢ (dom card = V → (𝑐 ∈ dom card ↔ 𝑐 ∈ V))
4	2, 3	mpbiri 258	. . . . 5 ⊢ (dom card = V → 𝑐 ∈ dom card)
5		infxpidm2 10034	. . . . . 6 ⊢ ((𝑐 ∈ dom card ∧ ω ≼ 𝑐) → (𝑐 × 𝑐) ≈ 𝑐)
6	5	ex 412	. . . . 5 ⊢ (𝑐 ∈ dom card → (ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐))
7	4, 6	syl 17	. . . 4 ⊢ (dom card = V → (ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐))
8	7	alrimiv 1923	. . 3 ⊢ (dom card = V → ∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐))
9		finnum 9965	. . . . . . 7 ⊢ (𝑎 ∈ Fin → 𝑎 ∈ dom card)
10	9	adantl 481	. . . . . 6 ⊢ ((∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ 𝑎 ∈ Fin) → 𝑎 ∈ dom card)
11		harcl 9576	. . . . . . . . 9 ⊢ (har‘𝑎) ∈ On
12		onenon 9966	. . . . . . . . 9 ⊢ ((har‘𝑎) ∈ On → (har‘𝑎) ∈ dom card)
13	11, 12	ax-mp 5	. . . . . . . 8 ⊢ (har‘𝑎) ∈ dom card
14		fvex 6904	. . . . . . . . . . . . . 14 ⊢ (har‘𝑎) ∈ V
15		vex 3474	. . . . . . . . . . . . . 14 ⊢ 𝑎 ∈ V
16	14, 15	unex 7742	. . . . . . . . . . . . 13 ⊢ ((har‘𝑎) ∪ 𝑎) ∈ V
17		harinf 42449	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ V ∧ ¬ 𝑎 ∈ Fin) → ω ⊆ (har‘𝑎))
18	15, 17	mpan 689	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑎 ∈ Fin → ω ⊆ (har‘𝑎))
19		ssun1 4168	. . . . . . . . . . . . . 14 ⊢ (har‘𝑎) ⊆ ((har‘𝑎) ∪ 𝑎)
20	18, 19	sstrdi 3990	. . . . . . . . . . . . 13 ⊢ (¬ 𝑎 ∈ Fin → ω ⊆ ((har‘𝑎) ∪ 𝑎))
21		ssdomg 9014	. . . . . . . . . . . . 13 ⊢ (((har‘𝑎) ∪ 𝑎) ∈ V → (ω ⊆ ((har‘𝑎) ∪ 𝑎) → ω ≼ ((har‘𝑎) ∪ 𝑎)))
22	16, 20, 21	mpsyl 68	. . . . . . . . . . . 12 ⊢ (¬ 𝑎 ∈ Fin → ω ≼ ((har‘𝑎) ∪ 𝑎))
23		breq2 5146	. . . . . . . . . . . . . 14 ⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → (ω ≼ 𝑐 ↔ ω ≼ ((har‘𝑎) ∪ 𝑎)))
24		xpeq12 5697	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = ((har‘𝑎) ∪ 𝑎) ∧ 𝑐 = ((har‘𝑎) ∪ 𝑎)) → (𝑐 × 𝑐) = (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)))
25	24	anidms 566	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → (𝑐 × 𝑐) = (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)))
26		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → 𝑐 = ((har‘𝑎) ∪ 𝑎))
27	25, 26	breq12d 5155	. . . . . . . . . . . . . 14 ⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → ((𝑐 × 𝑐) ≈ 𝑐 ↔ (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎)))
28	23, 27	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑐 = ((har‘𝑎) ∪ 𝑎) → ((ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ↔ (ω ≼ ((har‘𝑎) ∪ 𝑎) → (((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎))))
29	16, 28	spcv 3591	. . . . . . . . . . . 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 9579	. . . . . . . . . . . 12 ⊢ ¬ (har‘𝑎) ≼ 𝑎
33		ssdomg 9014	. . . . . . . . . . . . . 14 ⊢ (((har‘𝑎) ∪ 𝑎) ∈ V → ((har‘𝑎) ⊆ ((har‘𝑎) ∪ 𝑎) → (har‘𝑎) ≼ ((har‘𝑎) ∪ 𝑎)))
34	16, 19, 33	mp2 9	. . . . . . . . . . . . 13 ⊢ (har‘𝑎) ≼ ((har‘𝑎) ∪ 𝑎)
35		domtr 9021	. . . . . . . . . . . . 13 ⊢ (((har‘𝑎) ≼ ((har‘𝑎) ∪ 𝑎) ∧ ((har‘𝑎) ∪ 𝑎) ≼ 𝑎) → (har‘𝑎) ≼ 𝑎)
36	34, 35	mpan 689	. . . . . . . . . . . 12 ⊢ (((har‘𝑎) ∪ 𝑎) ≼ 𝑎 → (har‘𝑎) ≼ 𝑎)
37	32, 36	mto 196	. . . . . . . . . . 11 ⊢ ¬ ((har‘𝑎) ∪ 𝑎) ≼ 𝑎
38		unxpwdom2 9605	. . . . . . . . . . 11 ⊢ ((((har‘𝑎) ∪ 𝑎) × ((har‘𝑎) ∪ 𝑎)) ≈ ((har‘𝑎) ∪ 𝑎) → (((har‘𝑎) ∪ 𝑎) ≼^* (har‘𝑎) ∨ ((har‘𝑎) ∪ 𝑎) ≼ 𝑎))
39		orel2 889	. . . . . . . . . . 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 10081	. . . . . . . . . 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 10055	. . . . . . . 8 ⊢ (((har‘𝑎) ∈ dom card ∧ ((har‘𝑎) ∪ 𝑎) ≼ (har‘𝑎)) → ((har‘𝑎) ∪ 𝑎) ∈ dom card)
46	13, 44, 45	sylancr 586	. . . . . . 7 ⊢ ((∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ ¬ 𝑎 ∈ Fin) → ((har‘𝑎) ∪ 𝑎) ∈ dom card)
47		ssun2 4169	. . . . . . 7 ⊢ 𝑎 ⊆ ((har‘𝑎) ∪ 𝑎)
48		ssnum 10056	. . . . . . 7 ⊢ ((((har‘𝑎) ∪ 𝑎) ∈ dom card ∧ 𝑎 ⊆ ((har‘𝑎) ∪ 𝑎)) → 𝑎 ∈ dom card)
49	46, 47, 48	sylancl 585	. . . . . 6 ⊢ ((∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) ∧ ¬ 𝑎 ∈ Fin) → 𝑎 ∈ dom card)
50	10, 49	pm2.61dan 812	. . . . 5 ⊢ (∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) → 𝑎 ∈ dom card)
51	50	alrimiv 1923	. . . 4 ⊢ (∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐) → ∀𝑎 𝑎 ∈ dom card)
52		eqv 3479	. . . 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 846 ∀wal 1532 = wceq 1534 ∈ wcel 2099 Vcvv 3470 ∪ cun 3943 ⊆ wss 3945 class class class wbr 5142 × cxp 5670 dom cdm 5672 Oncon0 6363 ‘cfv 6542 ωcom 7864 ≈ cen 8954 ≼ cdom 8955 Fincfn 8957 harchar 9573 ≼^* cwdom 9581 cardccrd 9952 CHOICEwac 10132

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7734 ax-inf2 9658

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2937 df-ral 3058 df-rex 3067 df-rmo 3372 df-reu 3373 df-rab 3429 df-v 3472 df-sbc 3776 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3964 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-int 4945 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-se 5628 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-isom 6551 df-riota 7370 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7865 df-1st 7987 df-2nd 7988 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-er 8718 df-map 8840 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-oi 9527 df-har 9574 df-wdom 9582 df-card 9956 df-acn 9959 df-ac 10133

This theorem is referenced by: (None)

W3C validator