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 10083

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 2740	. 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 2827	. . . . 5 ⊢ (𝑠 = 𝑧 → (𝑠 ∈ (On × On) ↔ 𝑧 ∈ (On × On)))
3		eleq1w 2827	. . . . 5 ⊢ (𝑡 = 𝑤 → (𝑡 ∈ (On × On) ↔ 𝑤 ∈ (On × On)))
4	2, 3	bi2anan9 637	. . . 4 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((𝑠 ∈ (On × On) ∧ 𝑡 ∈ (On × On)) ↔ (𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On))))
5		fveq2 6920	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (1^st ‘𝑠) = (1^st ‘𝑧))
6		fveq2 6920	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (2^nd ‘𝑠) = (2^nd ‘𝑧))
7	5, 6	uneq12d 4192	. . . . . . 7 ⊢ (𝑠 = 𝑧 → ((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)))
8	7	adantr 480	. . . . . 6 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → ((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)))
9		fveq2 6920	. . . . . . . 8 ⊢ (𝑡 = 𝑤 → (1^st ‘𝑡) = (1^st ‘𝑤))
10		fveq2 6920	. . . . . . . 8 ⊢ (𝑡 = 𝑤 → (2^nd ‘𝑡) = (2^nd ‘𝑤))
11	9, 10	uneq12d 4192	. . . . . . 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 2838	. . . . 5 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) ∈ ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ↔ ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)) ∈ ((1^st ‘𝑤) ∪ (2^nd ‘𝑤))))
14	7, 11	eqeqan12d 2754	. . . . . 6 ⊢ ((𝑠 = 𝑧 ∧ 𝑡 = 𝑤) → (((1^st ‘𝑠) ∪ (2^nd ‘𝑠)) = ((1^st ‘𝑡) ∪ (2^nd ‘𝑡)) ↔ ((1^st ‘𝑧) ∪ (2^nd ‘𝑧)) = ((1^st ‘𝑤) ∪ (2^nd ‘𝑤))))
15		breq12 5171	. . . . . 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 631	. . . . 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 917	. . . 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 631	. . 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 5239	. 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 2740	. 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 2740	. 2 ⊢ ((1^st ‘𝑤) ∪ (2^nd ‘𝑤)) = ((1^st ‘𝑤) ∪ (2^nd ‘𝑤))
23		eqid 2740	. 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 10082	1 ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∨ wo 846 = wceq 1537 ∈ wcel 2108 ∀wral 3067 ∪ cun 3974 ∩ cin 3975 ⊆ wss 3976 class class class wbr 5166 {copab 5228 × cxp 5698 Oncon0 6395 ‘cfv 6573 ωcom 7903 1^st c1st 8028 2^nd c2nd 8029 ≈ cen 9000 ≺ csdm 9002 OrdIsocoi 9578

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-inf2 9710

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-se 5653 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-isom 6582 df-riota 7404 df-ov 7451 df-om 7904 df-1st 8030 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-1o 8522 df-er 8763 df-en 9004 df-dom 9005 df-sdom 9006 df-fin 9007 df-oi 9579 df-card 10008

This theorem is referenced by: xpomen 10084 infxpidm2 10086 alephreg 10651 cfpwsdom 10653 inar1 10844

W3C validator