Metamath Proof Explorer

Theorem opsrtoslem1

Description: Lemma for opsrtos . (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses opsrso.o ⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
opsrso.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
opsrso.r ⊢ ( 𝜑 → 𝑅 ∈ Toset )
opsrso.t ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
opsrso.w ⊢ ( 𝜑 → 𝑇 We 𝐼 )
opsrtoslem.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
opsrtoslem.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
opsrtoslem.q ⊢ < = ( lt ‘ 𝑅 )
opsrtoslem.c ⊢ 𝐶 = ( 𝑇 <bag 𝐼 )
opsrtoslem.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
opsrtoslem.ps ⊢ ( 𝜓 ↔ ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) )
opsrtoslem.l ⊢ ≤ = ( le ‘ 𝑂 )
Assertion opsrtoslem1 ( 𝜑 → ≤ = ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∪ ( I ↾ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 opsrso.o ⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
2 opsrso.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3 opsrso.r ⊢ ( 𝜑 → 𝑅 ∈ Toset )
4 opsrso.t ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
5 opsrso.w ⊢ ( 𝜑 → 𝑇 We 𝐼 )
6 opsrtoslem.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
7 opsrtoslem.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
8 opsrtoslem.q ⊢ < = ( lt ‘ 𝑅 )
9 opsrtoslem.c ⊢ 𝐶 = ( 𝑇 <bag 𝐼 )
10 opsrtoslem.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
11 opsrtoslem.ps ⊢ ( 𝜓 ↔ ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) )
12 opsrtoslem.l ⊢ ≤ = ( le ‘ 𝑂 )
13 6 1 7 8 9 10 12 4 opsrle ⊢ ( 𝜑 → ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } )
14 unopab ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) } ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) ∨ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) ) }
15 inopab ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜓 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) }
16 df-xp ⊢ ( 𝐵 × 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) }
17 16 ineq2i ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) } )
18 vex ⊢ 𝑥 ∈ V
19 vex ⊢ 𝑦 ∈ V
20 18 19 prss ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐵 )
21 20 anbi1i ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) )
22 ancom ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) ↔ ( 𝜓 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
23 21 22 bitr3i ⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) ↔ ( 𝜓 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
24 23 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜓 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) }
25 15 17 24 3eqtr4i ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) }
26 opabresid ⊢ ( I ↾ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) }
27 equcom ⊢ ( 𝑥 = 𝑦 ↔ 𝑦 = 𝑥 )
28 27 anbi2i ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝑦 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) )
29 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
30 29 biimpac ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝑦 ) → 𝑦 ∈ 𝐵 )
31 30 pm4.71i ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝑦 ) ∧ 𝑦 ∈ 𝐵 ) )
32 28 31 bitr3i ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝑦 ) ∧ 𝑦 ∈ 𝐵 ) )
33 an32 ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝑦 ) ∧ 𝑦 ∈ 𝐵 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 = 𝑦 ) )
34 20 anbi1i ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 = 𝑦 ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) )
35 32 33 34 3bitri ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) )
36 35 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) }
37 26 36 eqtri ⊢ ( I ↾ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) }
38 25 37 uneq12i ⊢ ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∪ ( I ↾ 𝐵 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) } ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) } )
39 11 orbi1i ⊢ ( ( 𝜓 ∨ 𝑥 = 𝑦 ) ↔ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) )
40 39 anbi2i ⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( 𝜓 ∨ 𝑥 = 𝑦 ) ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) )
41 andi ⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( 𝜓 ∨ 𝑥 = 𝑦 ) ) ↔ ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) ∨ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) ) )
42 40 41 bitr3i ⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) ↔ ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) ∨ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) ) )
43 42 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝜓 ) ∨ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ 𝑥 = 𝑦 ) ) }
44 14 38 43 3eqtr4ri ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } = ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∪ ( I ↾ 𝐵 ) )
45 13 44 syl6eq ⊢ ( 𝜑 → ≤ = ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∪ ( I ↾ 𝐵 ) ) )