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 9997

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 2769	. 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 2852	. . . . 5 ⊢ (𝑠 = 𝑧 → (𝑠 ∈ (On × On) ↔ 𝑧 ∈ (On × On)))
3		eleq1w 2852	. . . . 5 ⊢ (𝑡 = 𝑤 → (𝑡 ∈ (On × On) ↔ 𝑤 ∈ (On × On)))
4	2, 3	bi2anan9 649	. . . 4 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((𝑠 ∈ (On × On) ∧ 𝑡 ∈ (On × On)) ↔ (𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On))))
5		fveq2 6882	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (1^st ‘𝑠) = (1^st ‘𝑧))
6		fveq2 6882	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (2^nd ‘𝑠) = (2^nd ‘𝑧))
7	5, 6	uneq12d 4131	. . . . . . 7 ⊢ (𝑠 = 𝑧 → ((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)))
8	7	adantr 485	. . . . . 6 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)))
9		fveq2 6882	. . . . . . . 8 ⊢ (𝑡 = 𝑤 → (1^st ‘𝑡) = (1^st ‘𝑤))
10		fveq2 6882	. . . . . . . 8 ⊢ (𝑡 = 𝑤 → (2^nd ‘𝑡) = (2^nd ‘𝑤))
11	9, 10	uneq12d 4131	. . . . . . 7 ⊢ (𝑡 = 𝑤 → ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) = ((1^st ‘𝑤) ∪ (2^nd ‘𝑤)))
12	11	adantl 486	. . . . . 6 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) = ((1^st ‘𝑤) ∪ (2^nd ‘𝑤)))
13	8, 12	eleq12d 2863	. . . . 5 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) ∈ ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ↔ ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)) ∈ ((1^st ‘𝑤) ∪ (2^nd ‘𝑤))))
14	7, 11	eqeqan12d 2783	. . . . . 6 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ↔ ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)) = ((1^st ‘𝑤) ∪ (2^nd ‘𝑤))))
15		breq12 5118	. . . . . 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 643	. . . . 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 931	. . . 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 643	. . 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 5188	. 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 2769	. 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 264	. 2 ⊢ (((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)) ↔ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)))
22		eqid 2769	. 2 ⊢ ((1^st ‘𝑤) ∪ (2^nd ‘𝑤)) = ((1^st ‘𝑤) ∪ (2^nd ‘𝑤))
23		eqid 2769	. 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 9996	1 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 ∨ wo 860 = wceq 1567 ∈ wcel 2149 ∀wral 3085 ∪ cun 3911 ∩ cin 3912 ⊆ wss 3913 class class class wbr 5113 {copab 5177 × cxp 5660 Oncon0 6361 ‘cfv 6537 ωcom 7861 1^st c1st 7983 2^nd c2nd 7984 ≈ cen 8939 ≺ csdm 8941 OrdIsocoi 9470

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-inf2 9609

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-se 5616 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7368 df-ov 7414 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-er 8693 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-oi 9471 df-card 9924

This theorem is referenced by: xpomen 9998 infxpidm2 10000 alephreg 10566 cfpwsdom 10568 inar1 10759

W3C validator