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 9905

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 2731	. 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 2814	. . . . 5 ⊢ (𝑠 = 𝑧 → (𝑠 ∈ (On × On) ↔ 𝑧 ∈ (On × On)))
3		eleq1w 2814	. . . . 5 ⊢ (𝑡 = 𝑤 → (𝑡 ∈ (On × On) ↔ 𝑤 ∈ (On × On)))
4	2, 3	bi2anan9 638	. . . 4 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((𝑠 ∈ (On × On) ∧ 𝑡 ∈ (On × On)) ↔ (𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On))))
5		fveq2 6822	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (1^st ‘𝑠) = (1^st ‘𝑧))
6		fveq2 6822	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (2^nd ‘𝑠) = (2^nd ‘𝑧))
7	5, 6	uneq12d 4116	. . . . . . 7 ⊢ (𝑠 = 𝑧 → ((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)))
8	7	adantr 480	. . . . . 6 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)))
9		fveq2 6822	. . . . . . . 8 ⊢ (𝑡 = 𝑤 → (1^st ‘𝑡) = (1^st ‘𝑤))
10		fveq2 6822	. . . . . . . 8 ⊢ (𝑡 = 𝑤 → (2^nd ‘𝑡) = (2^nd ‘𝑤))
11	9, 10	uneq12d 4116	. . . . . . 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 2825	. . . . 5 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) ∈ ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ↔ ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)) ∈ ((1^st ‘𝑤) ∪ (2^nd ‘𝑤))))
14	7, 11	eqeqan12d 2745	. . . . . 6 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ↔ ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)) = ((1^st ‘𝑤) ∪ (2^nd ‘𝑤))))
15		breq12 5094	. . . . . 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 5162	. 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 2731	. 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 2731	. 2 ⊢ ((1^st ‘𝑤) ∪ (2^nd ‘𝑤)) = ((1^st ‘𝑤) ∪ (2^nd ‘𝑤))
23		eqid 2731	. 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 9904	1 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∨ wo 847 = wceq 1541 ∈ wcel 2111 ∀wral 3047 ∪ cun 3895 ∩ cin 3896 ⊆ wss 3897 class class class wbr 5089 {copab 5151 × cxp 5612 Oncon0 6306 ‘cfv 6481 ωcom 7796 1^st c1st 7919 2^nd c2nd 7920 ≈ cen 8866 ≺ csdm 8868 OrdIsocoi 9395

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-inf2 9531

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-int 4896 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-se 5568 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-isom 6490 df-riota 7303 df-ov 7349 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-oi 9396 df-card 9832

This theorem is referenced by: xpomen 9906 infxpidm2 9908 alephreg 10473 cfpwsdom 10475 inar1 10666

W3C validator