infxpen

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 R is a well-ordering of ( On X. On ) with the additional property that R -initial segments of ( x X. x ) (where x is a limit ordinal) are of cardinality at most x . (Contributed by Mario Carneiro, 9-Mar-2013) (Revised by Mario Carneiro, 26-Jun-2015)

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

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 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	⊢ ( 𝑠 = 𝑧 → ( 𝑠 ∈ ( On × On ) ↔ 𝑧 ∈ ( On × On ) ) )
3		eleq1w	⊢ ( 𝑡 = 𝑤 → ( 𝑡 ∈ ( On × On ) ↔ 𝑤 ∈ ( On × On ) ) )
4	2 3	bi2anan9	⊢ ( ( 𝑠 = 𝑧 ∧ 𝑡 = 𝑤 ) → ( ( 𝑠 ∈ ( On × On ) ∧ 𝑡 ∈ ( On × On ) ) ↔ ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) ) )
5		fveq2	⊢ ( 𝑠 = 𝑧 → ( 1^st ‘ 𝑠 ) = ( 1^st ‘ 𝑧 ) )
6		fveq2	⊢ ( 𝑠 = 𝑧 → ( 2^nd ‘ 𝑠 ) = ( 2^nd ‘ 𝑧 ) )
7	5 6	uneq12d	⊢ ( 𝑠 = 𝑧 → ( ( 1^st ‘ 𝑠 ) ∪ ( 2^nd ‘ 𝑠 ) ) = ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) )
8	7	adantr	⊢ ( ( 𝑠 = 𝑧 ∧ 𝑡 = 𝑤 ) → ( ( 1^st ‘ 𝑠 ) ∪ ( 2^nd ‘ 𝑠 ) ) = ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) )
9		fveq2	⊢ ( 𝑡 = 𝑤 → ( 1^st ‘ 𝑡 ) = ( 1^st ‘ 𝑤 ) )
10		fveq2	⊢ ( 𝑡 = 𝑤 → ( 2^nd ‘ 𝑡 ) = ( 2^nd ‘ 𝑤 ) )
11	9 10	uneq12d	⊢ ( 𝑡 = 𝑤 → ( ( 1^st ‘ 𝑡 ) ∪ ( 2^nd ‘ 𝑡 ) ) = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) )
12	11	adantl	⊢ ( ( 𝑠 = 𝑧 ∧ 𝑡 = 𝑤 ) → ( ( 1^st ‘ 𝑡 ) ∪ ( 2^nd ‘ 𝑡 ) ) = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) )
13	8 12	eleq12d	⊢ ( ( 𝑠 = 𝑧 ∧ 𝑡 = 𝑤 ) → ( ( ( 1^st ‘ 𝑠 ) ∪ ( 2^nd ‘ 𝑠 ) ) ∈ ( ( 1^st ‘ 𝑡 ) ∪ ( 2^nd ‘ 𝑡 ) ) ↔ ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ∈ ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ) )
14	7 11	eqeqan12d	⊢ ( ( 𝑠 = 𝑧 ∧ 𝑡 = 𝑤 ) → ( ( ( 1^st ‘ 𝑠 ) ∪ ( 2^nd ‘ 𝑠 ) ) = ( ( 1^st ‘ 𝑡 ) ∪ ( 2^nd ‘ 𝑡 ) ) ↔ ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ) )
15		breq12	⊢ ( ( 𝑠 = 𝑧 ∧ 𝑡 = 𝑤 ) → ( 𝑠 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 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	⊢ ( ( 𝑠 = 𝑧 ∧ 𝑡 = 𝑤 ) → ( ( ( ( 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	⊢ ( ( 𝑠 = 𝑧 ∧ 𝑡 = 𝑤 ) → ( ( ( ( 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	⊢ ( ( 𝑠 = 𝑧 ∧ 𝑡 = 𝑤 ) → ( ( ( 𝑠 ∈ ( 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	⊢ { ⟨ 𝑠 , 𝑡 ⟩ ∣ ( ( 𝑠 ∈ ( 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	⊢ ( { ⟨ 𝑠 , 𝑡 ⟩ ∣ ( ( 𝑠 ∈ ( 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	⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) ↔ ( ( 𝑎 ∈ On ∧ ∀ 𝑚 ∈ 𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ∀ 𝑚 ∈ 𝑎 𝑚 ≺ 𝑎 ) ) )
22		eqid	⊢ ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) )
23		eqid	⊢ 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	⊢ ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 )

Metamath Proof Explorer

Theorem infxpen

Proof