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 𝐷 = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ 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 𝐷 = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ 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 eqtrdi ( 𝜑 = ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∪ ( I ↾ 𝐵 ) ) )