Metamath Proof Explorer


Theorem 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 ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) }
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 ( 𝑠 = 𝑧 → ( 1st𝑠 ) = ( 1st𝑧 ) )
6 fveq2 ( 𝑠 = 𝑧 → ( 2nd𝑠 ) = ( 2nd𝑧 ) )
7 5 6 uneq12d ( 𝑠 = 𝑧 → ( ( 1st𝑠 ) ∪ ( 2nd𝑠 ) ) = ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) )
8 7 adantr ( ( 𝑠 = 𝑧𝑡 = 𝑤 ) → ( ( 1st𝑠 ) ∪ ( 2nd𝑠 ) ) = ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) )
9 fveq2 ( 𝑡 = 𝑤 → ( 1st𝑡 ) = ( 1st𝑤 ) )
10 fveq2 ( 𝑡 = 𝑤 → ( 2nd𝑡 ) = ( 2nd𝑤 ) )
11 9 10 uneq12d ( 𝑡 = 𝑤 → ( ( 1st𝑡 ) ∪ ( 2nd𝑡 ) ) = ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) )
12 11 adantl ( ( 𝑠 = 𝑧𝑡 = 𝑤 ) → ( ( 1st𝑡 ) ∪ ( 2nd𝑡 ) ) = ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) )
13 8 12 eleq12d ( ( 𝑠 = 𝑧𝑡 = 𝑤 ) → ( ( ( 1st𝑠 ) ∪ ( 2nd𝑠 ) ) ∈ ( ( 1st𝑡 ) ∪ ( 2nd𝑡 ) ) ↔ ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ∈ ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ) )
14 7 11 eqeqan12d ( ( 𝑠 = 𝑧𝑡 = 𝑤 ) → ( ( ( 1st𝑠 ) ∪ ( 2nd𝑠 ) ) = ( ( 1st𝑡 ) ∪ ( 2nd𝑡 ) ) ↔ ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) = ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ) )
15 breq12 ( ( 𝑠 = 𝑧𝑡 = 𝑤 ) → ( 𝑠 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) } 𝑡𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) } 𝑤 ) )
16 14 15 anbi12d ( ( 𝑠 = 𝑧𝑡 = 𝑤 ) → ( ( ( ( 1st𝑠 ) ∪ ( 2nd𝑠 ) ) = ( ( 1st𝑡 ) ∪ ( 2nd𝑡 ) ) ∧ 𝑠 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) } 𝑡 ) ↔ ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) = ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ∧ 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) } 𝑤 ) ) )
17 13 16 orbi12d ( ( 𝑠 = 𝑧𝑡 = 𝑤 ) → ( ( ( ( 1st𝑠 ) ∪ ( 2nd𝑠 ) ) ∈ ( ( 1st𝑡 ) ∪ ( 2nd𝑡 ) ) ∨ ( ( ( 1st𝑠 ) ∪ ( 2nd𝑠 ) ) = ( ( 1st𝑡 ) ∪ ( 2nd𝑡 ) ) ∧ 𝑠 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) } 𝑡 ) ) ↔ ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ∈ ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ∨ ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) = ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ∧ 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) } 𝑤 ) ) ) )
18 4 17 anbi12d ( ( 𝑠 = 𝑧𝑡 = 𝑤 ) → ( ( ( 𝑠 ∈ ( On × On ) ∧ 𝑡 ∈ ( On × On ) ) ∧ ( ( ( 1st𝑠 ) ∪ ( 2nd𝑠 ) ) ∈ ( ( 1st𝑡 ) ∪ ( 2nd𝑡 ) ) ∨ ( ( ( 1st𝑠 ) ∪ ( 2nd𝑠 ) ) = ( ( 1st𝑡 ) ∪ ( 2nd𝑡 ) ) ∧ 𝑠 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) } 𝑡 ) ) ) ↔ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) ∧ ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ∈ ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ∨ ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) = ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ∧ 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) } 𝑤 ) ) ) ) )
19 18 cbvopabv { ⟨ 𝑠 , 𝑡 ⟩ ∣ ( ( 𝑠 ∈ ( On × On ) ∧ 𝑡 ∈ ( On × On ) ) ∧ ( ( ( 1st𝑠 ) ∪ ( 2nd𝑠 ) ) ∈ ( ( 1st𝑡 ) ∪ ( 2nd𝑡 ) ) ∨ ( ( ( 1st𝑠 ) ∪ ( 2nd𝑠 ) ) = ( ( 1st𝑡 ) ∪ ( 2nd𝑡 ) ) ∧ 𝑠 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) } 𝑡 ) ) ) } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) ∧ ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ∈ ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ∨ ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) = ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) ∧ 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) } 𝑤 ) ) ) }
20 eqid ( { ⟨ 𝑠 , 𝑡 ⟩ ∣ ( ( 𝑠 ∈ ( On × On ) ∧ 𝑡 ∈ ( On × On ) ) ∧ ( ( ( 1st𝑠 ) ∪ ( 2nd𝑠 ) ) ∈ ( ( 1st𝑡 ) ∪ ( 2nd𝑡 ) ) ∨ ( ( ( 1st𝑠 ) ∪ ( 2nd𝑠 ) ) = ( ( 1st𝑡 ) ∪ ( 2nd𝑡 ) ) ∧ 𝑠 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) } 𝑡 ) ) ) } ∩ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) ) = ( { ⟨ 𝑠 , 𝑡 ⟩ ∣ ( ( 𝑠 ∈ ( On × On ) ∧ 𝑡 ∈ ( On × On ) ) ∧ ( ( ( 1st𝑠 ) ∪ ( 2nd𝑠 ) ) ∈ ( ( 1st𝑡 ) ∪ ( 2nd𝑡 ) ) ∨ ( ( ( 1st𝑠 ) ∪ ( 2nd𝑠 ) ) = ( ( 1st𝑡 ) ∪ ( 2nd𝑡 ) ) ∧ 𝑠 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) } 𝑡 ) ) ) } ∩ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) )
21 biid ( ( ( 𝑎 ∈ On ∧ ∀ 𝑚𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ∀ 𝑚𝑎 𝑚𝑎 ) ) ↔ ( ( 𝑎 ∈ On ∧ ∀ 𝑚𝑎 ( ω ⊆ 𝑚 → ( 𝑚 × 𝑚 ) ≈ 𝑚 ) ) ∧ ( ω ⊆ 𝑎 ∧ ∀ 𝑚𝑎 𝑚𝑎 ) ) )
22 eqid ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) ) = ( ( 1st𝑤 ) ∪ ( 2nd𝑤 ) )
23 eqid OrdIso ( ( { ⟨ 𝑠 , 𝑡 ⟩ ∣ ( ( 𝑠 ∈ ( On × On ) ∧ 𝑡 ∈ ( On × On ) ) ∧ ( ( ( 1st𝑠 ) ∪ ( 2nd𝑠 ) ) ∈ ( ( 1st𝑡 ) ∪ ( 2nd𝑡 ) ) ∨ ( ( ( 1st𝑠 ) ∪ ( 2nd𝑠 ) ) = ( ( 1st𝑡 ) ∪ ( 2nd𝑡 ) ) ∧ 𝑠 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) } 𝑡 ) ) ) } ∩ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) ) , ( 𝑎 × 𝑎 ) ) = OrdIso ( ( { ⟨ 𝑠 , 𝑡 ⟩ ∣ ( ( 𝑠 ∈ ( On × On ) ∧ 𝑡 ∈ ( On × On ) ) ∧ ( ( ( 1st𝑠 ) ∪ ( 2nd𝑠 ) ) ∈ ( ( 1st𝑡 ) ∪ ( 2nd𝑡 ) ) ∨ ( ( ( 1st𝑠 ) ∪ ( 2nd𝑠 ) ) = ( ( 1st𝑡 ) ∪ ( 2nd𝑡 ) ) ∧ 𝑠 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) } 𝑡 ) ) ) } ∩ ( ( 𝑎 × 𝑎 ) × ( 𝑎 × 𝑎 ) ) ) , ( 𝑎 × 𝑎 ) )
24 1 19 20 21 22 23 infxpenlem ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 )