Metamath Proof Explorer


Theorem leweon

Description: Lexicographical order is a well-ordering of On X. On . Proposition 7.56(1) of TakeutiZaring p. 54. Note that unlike r0weon , this order isnot set-like, as the preimage of <. 1o , (/) >. is the proper class ( { (/) } X. On ) . (Contributed by Mario Carneiro, 9-Mar-2013)

Ref Expression
Hypothesis leweon.1 𝐿 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) }
Assertion leweon 𝐿 We ( On × On )

Proof

Step Hyp Ref Expression
1 leweon.1 𝐿 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) }
2 epweon E We On
3 fvex ( 1st𝑦 ) ∈ V
4 3 epeli ( ( 1st𝑥 ) E ( 1st𝑦 ) ↔ ( 1st𝑥 ) ∈ ( 1st𝑦 ) )
5 fvex ( 2nd𝑦 ) ∈ V
6 5 epeli ( ( 2nd𝑥 ) E ( 2nd𝑦 ) ↔ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) )
7 6 anbi2i ( ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) E ( 2nd𝑦 ) ) ↔ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) )
8 4 7 orbi12i ( ( ( 1st𝑥 ) E ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) E ( 2nd𝑦 ) ) ) ↔ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) )
9 8 anbi2i ( ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) E ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) E ( 2nd𝑦 ) ) ) ) ↔ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) )
10 9 opabbii { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) E ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) E ( 2nd𝑦 ) ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) ∈ ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) ∈ ( 2nd𝑦 ) ) ) ) }
11 1 10 eqtr4i 𝐿 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st𝑥 ) E ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) E ( 2nd𝑦 ) ) ) ) }
12 11 wexp ( ( E We On ∧ E We On ) → 𝐿 We ( On × On ) )
13 2 2 12 mp2an 𝐿 We ( On × On )