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 ) ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) ∈ ( 2^nd ‘ 𝑦 ) ) ) ) }
	Assertion	leweon	⊢ 𝐿 We ( On × On )

Proof

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

Metamath Proof Explorer

Theorem leweon

Proof