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 9936

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 2737	. 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 2820	. . . . 5 ⊢ (𝑠 = 𝑧 → (𝑠 ∈ (On × On) ↔ 𝑧 ∈ (On × On)))
3		eleq1w 2820	. . . . 5 ⊢ (𝑡 = 𝑤 → (𝑡 ∈ (On × On) ↔ 𝑤 ∈ (On × On)))
4	2, 3	bi2anan9 639	. . . 4 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((𝑠 ∈ (On × On) ∧ 𝑡 ∈ (On × On)) ↔ (𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On))))
5		fveq2 6842	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (1^st ‘𝑠) = (1^st ‘𝑧))
6		fveq2 6842	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (2^nd ‘𝑠) = (2^nd ‘𝑧))
7	5, 6	uneq12d 4123	. . . . . . 7 ⊢ (𝑠 = 𝑧 → ((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)))
8	7	adantr 480	. . . . . 6 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)))
9		fveq2 6842	. . . . . . . 8 ⊢ (𝑡 = 𝑤 → (1^st ‘𝑡) = (1^st ‘𝑤))
10		fveq2 6842	. . . . . . . 8 ⊢ (𝑡 = 𝑤 → (2^nd ‘𝑡) = (2^nd ‘𝑤))
11	9, 10	uneq12d 4123	. . . . . . 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 2831	. . . . 5 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) ∈ ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ↔ ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)) ∈ ((1^st ‘𝑤) ∪ (2^nd ‘𝑤))))
14	7, 11	eqeqan12d 2751	. . . . . 6 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ↔ ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)) = ((1^st ‘𝑤) ∪ (2^nd ‘𝑤))))
15		breq12 5105	. . . . . 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 633	. . . . 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 919	. . . 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 633	. . 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 5173	. 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 2737	. 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 2737	. 2 ⊢ ((1^st ‘𝑤) ∪ (2^nd ‘𝑤)) = ((1^st ‘𝑤) ∪ (2^nd ‘𝑤))
23		eqid 2737	. 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 9935	1 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∨ wo 848 = wceq 1542 ∈ wcel 2114 ∀wral 3052 ∪ cun 3901 ∩ cin 3902 ⊆ wss 3903 class class class wbr 5100 {copab 5162 × cxp 5630 Oncon0 6325 ‘cfv 6500 ωcom 7818 1^st c1st 7941 2^nd c2nd 7942 ≈ cen 8892 ≺ csdm 8894 OrdIsocoi 9426

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-inf2 9562

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-se 5586 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-isom 6509 df-riota 7325 df-ov 7371 df-om 7819 df-1st 7943 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-er 8645 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-oi 9427 df-card 9863

This theorem is referenced by: xpomen 9937 infxpidm2 9939 alephreg 10505 cfpwsdom 10507 inar1 10698

W3C validator