infxpen - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > infxpen		Structured version Visualization version GIF version

Theorem infxpen 9943

Description: Every infinite ordinal is equinumerous to its Cartesian square. Proposition 10.39 of [TakeutiZaring] p. 94, whose proof we follow closely. The key idea is to show that the relation 𝑅 is a well-ordering of (On × On) with the additional property that 𝑅-initial segments of (𝑥 × 𝑥) (where 𝑥 is a limit ordinal) are of cardinality at most 𝑥. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.)

**Assertion**
Ref	Expression
infxpen	⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)

Proof of Theorem infxpen Dummy variables 𝑚 𝑎 𝑠 𝑡 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2729	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1^st ‘𝑥) ∈ (1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) ∈ (2^nd ‘𝑦))))} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1^st ‘𝑥) ∈ (1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) ∈ (2^nd ‘𝑦))))}
2		eleq1w 2811	. . . . 5 ⊢ (𝑠 = 𝑧 → (𝑠 ∈ (On × On) ↔ 𝑧 ∈ (On × On)))
3		eleq1w 2811	. . . . 5 ⊢ (𝑡 = 𝑤 → (𝑡 ∈ (On × On) ↔ 𝑤 ∈ (On × On)))
4	2, 3	bi2anan9 638	. . . 4 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((𝑠 ∈ (On × On) ∧ 𝑡 ∈ (On × On)) ↔ (𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On))))
5		fveq2 6840	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (1^st ‘𝑠) = (1^st ‘𝑧))
6		fveq2 6840	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (2^nd ‘𝑠) = (2^nd ‘𝑧))
7	5, 6	uneq12d 4128	. . . . . . 7 ⊢ (𝑠 = 𝑧 → ((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)))
8	7	adantr 480	. . . . . 6 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)))
9		fveq2 6840	. . . . . . . 8 ⊢ (𝑡 = 𝑤 → (1^st ‘𝑡) = (1^st ‘𝑤))
10		fveq2 6840	. . . . . . . 8 ⊢ (𝑡 = 𝑤 → (2^nd ‘𝑡) = (2^nd ‘𝑤))
11	9, 10	uneq12d 4128	. . . . . . 7 ⊢ (𝑡 = 𝑤 → ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) = ((1^st ‘𝑤) ∪ (2^nd ‘𝑤)))
12	11	adantl 481	. . . . . 6 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) = ((1^st ‘𝑤) ∪ (2^nd ‘𝑤)))
13	8, 12	eleq12d 2822	. . . . 5 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) ∈ ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ↔ ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)) ∈ ((1^st ‘𝑤) ∪ (2^nd ‘𝑤))))
14	7, 11	eqeqan12d 2743	. . . . . 6 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ↔ ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)) = ((1^st ‘𝑤) ∪ (2^nd ‘𝑤))))
15		breq12 5107	. . . . . 6 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (𝑠{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1^st ‘𝑥) ∈ (1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) ∈ (2^nd ‘𝑦))))}𝑡 ↔ 𝑧{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1^st ‘𝑥) ∈ (1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) ∈ (2^nd ‘𝑦))))}𝑤))
16	14, 15	anbi12d 632	. . . . 5 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ∧ 𝑠{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1^st ‘𝑥) ∈ (1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) ∈ (2^nd ‘𝑦))))}𝑡) ↔ (((1^st ‘𝑧) ∪ (2^nd ‘𝑧)) = ((1^st ‘𝑤) ∪ (2^nd ‘𝑤)) ∧ 𝑧{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1^st ‘𝑥) ∈ (1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) ∈ (2^nd ‘𝑦))))}𝑤)))
17	13, 16	orbi12d 918	. . . 4 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) ∈ ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ∨ (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ∧ 𝑠{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1^st ‘𝑥) ∈ (1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) ∈ (2^nd ‘𝑦))))}𝑡)) ↔ (((1^st ‘𝑧) ∪ (2^nd ‘𝑧)) ∈ ((1^st ‘𝑤) ∪ (2^nd ‘𝑤)) ∨ (((1^st ‘𝑧) ∪ (2^nd ‘𝑧)) = ((1^st ‘𝑤) ∪ (2^nd ‘𝑤)) ∧ 𝑧{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1^st ‘𝑥) ∈ (1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) ∈ (2^nd ‘𝑦))))}𝑤))))
18	4, 17	anbi12d 632	. . 3 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (((𝑠 ∈ (On × On) ∧ 𝑡 ∈ (On × On)) ∧ (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) ∈ ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ∨ (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ∧ 𝑠{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1^st ‘𝑥) ∈ (1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) ∈ (2^nd ‘𝑦))))}𝑡))) ↔ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1^st ‘𝑧) ∪ (2^nd ‘𝑧)) ∈ ((1^st ‘𝑤) ∪ (2^nd ‘𝑤)) ∨ (((1^st ‘𝑧) ∪ (2^nd ‘𝑧)) = ((1^st ‘𝑤) ∪ (2^nd ‘𝑤)) ∧ 𝑧{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1^st ‘𝑥) ∈ (1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) ∈ (2^nd ‘𝑦))))}𝑤)))))
19	18	cbvopabv 5175	. 2 ⊢ {⟨𝑠, 𝑡⟩ ∣ ((𝑠 ∈ (On × On) ∧ 𝑡 ∈ (On × On)) ∧ (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) ∈ ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ∨ (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ∧ 𝑠{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1^st ‘𝑥) ∈ (1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) ∈ (2^nd ‘𝑦))))}𝑡)))} = {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1^st ‘𝑧) ∪ (2^nd ‘𝑧)) ∈ ((1^st ‘𝑤) ∪ (2^nd ‘𝑤)) ∨ (((1^st ‘𝑧) ∪ (2^nd ‘𝑧)) = ((1^st ‘𝑤) ∪ (2^nd ‘𝑤)) ∧ 𝑧{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1^st ‘𝑥) ∈ (1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) ∈ (2^nd ‘𝑦))))}𝑤)))}
20		eqid 2729	. 2 ⊢ ({⟨𝑠, 𝑡⟩ ∣ ((𝑠 ∈ (On × On) ∧ 𝑡 ∈ (On × On)) ∧ (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) ∈ ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ∨ (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ∧ 𝑠{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1^st ‘𝑥) ∈ (1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) ∈ (2^nd ‘𝑦))))}𝑡)))} ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) = ({⟨𝑠, 𝑡⟩ ∣ ((𝑠 ∈ (On × On) ∧ 𝑡 ∈ (On × On)) ∧ (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) ∈ ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ∨ (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ∧ 𝑠{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1^st ‘𝑥) ∈ (1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) ∈ (2^nd ‘𝑦))))}𝑡)))} ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))
21		biid 261	. 2 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) ↔ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)))
22		eqid 2729	. 2 ⊢ ((1^st ‘𝑤) ∪ (2^nd ‘𝑤)) = ((1^st ‘𝑤) ∪ (2^nd ‘𝑤))
23		eqid 2729	. 2 ⊢ OrdIso(({⟨𝑠, 𝑡⟩ ∣ ((𝑠 ∈ (On × On) ∧ 𝑡 ∈ (On × On)) ∧ (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) ∈ ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ∨ (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ∧ 𝑠{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1^st ‘𝑥) ∈ (1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) ∈ (2^nd ‘𝑦))))}𝑡)))} ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))), (𝑎 × 𝑎)) = OrdIso(({⟨𝑠, 𝑡⟩ ∣ ((𝑠 ∈ (On × On) ∧ 𝑡 ∈ (On × On)) ∧ (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) ∈ ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ∨ (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ∧ 𝑠{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1^st ‘𝑥) ∈ (1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥) ∈ (2^nd ‘𝑦))))}𝑡)))} ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))), (𝑎 × 𝑎))
24	1, 19, 20, 21, 22, 23	infxpenlem 9942	1 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∨ wo 847 = wceq 1540 ∈ wcel 2109 ∀wral 3044 ∪ cun 3909 ∩ cin 3910 ⊆ wss 3911 class class class wbr 5102 {copab 5164 × cxp 5629 Oncon0 6320 ‘cfv 6499 ωcom 7822 1^st c1st 7945 2^nd c2nd 7946 ≈ cen 8892 ≺ csdm 8894 OrdIsocoi 9438

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-inf2 9570

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7326 df-ov 7372 df-om 7823 df-1st 7947 df-2nd 7948 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-er 8648 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-oi 9439 df-card 9868

This theorem is referenced by: xpomen 9944 infxpidm2 9946 alephreg 10511 cfpwsdom 10513 inar1 10704

W3C validator