Metamath Proof Explorer

Theorem thlle

Description: Ordering on the Hilbert lattice of closed subspaces. (Contributed by Mario Carneiro, 25-Oct-2015) (Proof shortened by AV, 11-Nov-2024)

Ref Expression
Hypotheses thlval.k ⊢ 𝐾 = ( toHL ‘ 𝑊 )
thlbas.c ⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
thlle.i ⊢ 𝐼 = ( toInc ‘ 𝐶 )
thlle.l ⊢ ≤ = ( le ‘ 𝐼 )
Assertion thlle ≤ = ( le ‘ 𝐾 )

Proof

Step Hyp Ref Expression
1 thlval.k ⊢ 𝐾 = ( toHL ‘ 𝑊 )
2 thlbas.c ⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
3 thlle.i ⊢ 𝐼 = ( toInc ‘ 𝐶 )
4 thlle.l ⊢ ≤ = ( le ‘ 𝐼 )
5 pleid ⊢ le = Slot ( le ‘ ndx )
6 plendxnocndx ⊢ ( le ‘ ndx ) ≠ ( oc ‘ ndx )
7 5 6 setsnid ⊢ ( le ‘ 𝐼 ) = ( le ‘ ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) )
8 4 7 eqtri ⊢ ≤ = ( le ‘ ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) )
9 eqid ⊢ ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
10 1 2 3 9 thlval ⊢ ( 𝑊 ∈ V → 𝐾 = ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) )
11 10 fveq2d ⊢ ( 𝑊 ∈ V → ( le ‘ 𝐾 ) = ( le ‘ ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) ) )
12 8 11 eqtr4id ⊢ ( 𝑊 ∈ V → ≤ = ( le ‘ 𝐾 ) )
13 5 str0 ⊢ ∅ = ( le ‘ ∅ )
14 2 fvexi ⊢ 𝐶 ∈ V
15 3 ipolerval ⊢ ( 𝐶 ∈ V → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) } = ( le ‘ 𝐼 ) )
16 14 15 ax-mp ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) } = ( le ‘ 𝐼 )
17 4 16 eqtr4i ⊢ ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) }
18 opabn0 ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) } ≠ ∅ ↔ ∃ 𝑥 ∃ 𝑦 ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) )
19 vex ⊢ 𝑥 ∈ V
20 vex ⊢ 𝑦 ∈ V
21 19 20 prss ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐶 )
22 elfvex ⊢ ( 𝑥 ∈ ( ClSubSp ‘ 𝑊 ) → 𝑊 ∈ V )
23 22 2 eleq2s ⊢ ( 𝑥 ∈ 𝐶 → 𝑊 ∈ V )
24 23 ad2antrr ⊢ ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ⊆ 𝑦 ) → 𝑊 ∈ V )
25 21 24 sylanbr ⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) → 𝑊 ∈ V )
26 25 exlimivv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) → 𝑊 ∈ V )
27 18 26 sylbi ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) } ≠ ∅ → 𝑊 ∈ V )
28 27 necon1bi ⊢ ( ¬ 𝑊 ∈ V → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) } = ∅ )
29 17 28 eqtrid ⊢ ( ¬ 𝑊 ∈ V → ≤ = ∅ )
30 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( toHL ‘ 𝑊 ) = ∅ )
31 1 30 eqtrid ⊢ ( ¬ 𝑊 ∈ V → 𝐾 = ∅ )
32 31 fveq2d ⊢ ( ¬ 𝑊 ∈ V → ( le ‘ 𝐾 ) = ( le ‘ ∅ ) )
33 13 29 32 3eqtr4a ⊢ ( ¬ 𝑊 ∈ V → ≤ = ( le ‘ 𝐾 ) )
34 12 33 pm2.61i ⊢ ≤ = ( le ‘ 𝐾 )