Metamath Proof Explorer


Theorem cvmlift2lem1

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 1-Jun-2015)

Ref Expression
Assertion cvmlift2lem1 ( ∀ 𝑦 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ( ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 → ( ( 0 [,] 1 ) × { 𝑡 } ) ⊆ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 biimp ( ( ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → ( ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 → ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) )
2 iitop II ∈ Top
3 iiuni ( 0 [,] 1 ) = II
4 3 neii1 ( ( II ∈ Top ∧ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → 𝑢 ⊆ ( 0 [,] 1 ) )
5 2 4 mpan ( 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) → 𝑢 ⊆ ( 0 [,] 1 ) )
6 5 adantl ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → 𝑢 ⊆ ( 0 [,] 1 ) )
7 xpss1 ( 𝑢 ⊆ ( 0 [,] 1 ) → ( 𝑢 × { 𝑥 } ) ⊆ ( ( 0 [,] 1 ) × { 𝑥 } ) )
8 6 7 syl ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → ( 𝑢 × { 𝑥 } ) ⊆ ( ( 0 [,] 1 ) × { 𝑥 } ) )
9 simpl ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 )
10 8 9 sstrd ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 )
11 ssnei ( ( II ∈ Top ∧ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → { 𝑦 } ⊆ 𝑢 )
12 2 11 mpan ( 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) → { 𝑦 } ⊆ 𝑢 )
13 12 adantl ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → { 𝑦 } ⊆ 𝑢 )
14 vex 𝑦 ∈ V
15 14 snss ( 𝑦𝑢 ↔ { 𝑦 } ⊆ 𝑢 )
16 13 15 sylibr ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → 𝑦𝑢 )
17 vsnid 𝑡 ∈ { 𝑡 }
18 opelxpi ( ( 𝑦𝑢𝑡 ∈ { 𝑡 } ) → ⟨ 𝑦 , 𝑡 ⟩ ∈ ( 𝑢 × { 𝑡 } ) )
19 16 17 18 sylancl ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → ⟨ 𝑦 , 𝑡 ⟩ ∈ ( 𝑢 × { 𝑡 } ) )
20 ssel ( ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 → ( ⟨ 𝑦 , 𝑡 ⟩ ∈ ( 𝑢 × { 𝑡 } ) → ⟨ 𝑦 , 𝑡 ⟩ ∈ 𝑀 ) )
21 19 20 syl5com ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → ( ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 → ⟨ 𝑦 , 𝑡 ⟩ ∈ 𝑀 ) )
22 10 21 embantd ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → ( ( ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 → ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → ⟨ 𝑦 , 𝑡 ⟩ ∈ 𝑀 ) )
23 1 22 syl5 ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ) → ( ( ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → ⟨ 𝑦 , 𝑡 ⟩ ∈ 𝑀 ) )
24 23 rexlimdva ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 → ( ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ( ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → ⟨ 𝑦 , 𝑡 ⟩ ∈ 𝑀 ) )
25 24 ralimdv ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 → ( ∀ 𝑦 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ( ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → ∀ 𝑦 ∈ ( 0 [,] 1 ) ⟨ 𝑦 , 𝑡 ⟩ ∈ 𝑀 ) )
26 25 com12 ( ∀ 𝑦 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ( ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 → ∀ 𝑦 ∈ ( 0 [,] 1 ) ⟨ 𝑦 , 𝑡 ⟩ ∈ 𝑀 ) )
27 dfss3 ( ( ( 0 [,] 1 ) × { 𝑡 } ) ⊆ 𝑀 ↔ ∀ 𝑧 ∈ ( ( 0 [,] 1 ) × { 𝑡 } ) 𝑧𝑀 )
28 eleq1 ( 𝑧 = ⟨ 𝑦 , 𝑢 ⟩ → ( 𝑧𝑀 ↔ ⟨ 𝑦 , 𝑢 ⟩ ∈ 𝑀 ) )
29 28 ralxp ( ∀ 𝑧 ∈ ( ( 0 [,] 1 ) × { 𝑡 } ) 𝑧𝑀 ↔ ∀ 𝑦 ∈ ( 0 [,] 1 ) ∀ 𝑢 ∈ { 𝑡 } ⟨ 𝑦 , 𝑢 ⟩ ∈ 𝑀 )
30 vex 𝑡 ∈ V
31 opeq2 ( 𝑢 = 𝑡 → ⟨ 𝑦 , 𝑢 ⟩ = ⟨ 𝑦 , 𝑡 ⟩ )
32 31 eleq1d ( 𝑢 = 𝑡 → ( ⟨ 𝑦 , 𝑢 ⟩ ∈ 𝑀 ↔ ⟨ 𝑦 , 𝑡 ⟩ ∈ 𝑀 ) )
33 30 32 ralsn ( ∀ 𝑢 ∈ { 𝑡 } ⟨ 𝑦 , 𝑢 ⟩ ∈ 𝑀 ↔ ⟨ 𝑦 , 𝑡 ⟩ ∈ 𝑀 )
34 33 ralbii ( ∀ 𝑦 ∈ ( 0 [,] 1 ) ∀ 𝑢 ∈ { 𝑡 } ⟨ 𝑦 , 𝑢 ⟩ ∈ 𝑀 ↔ ∀ 𝑦 ∈ ( 0 [,] 1 ) ⟨ 𝑦 , 𝑡 ⟩ ∈ 𝑀 )
35 27 29 34 3bitri ( ( ( 0 [,] 1 ) × { 𝑡 } ) ⊆ 𝑀 ↔ ∀ 𝑦 ∈ ( 0 [,] 1 ) ⟨ 𝑦 , 𝑡 ⟩ ∈ 𝑀 )
36 26 35 syl6ibr ( ∀ 𝑦 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ( ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 → ( ( 0 [,] 1 ) × { 𝑡 } ) ⊆ 𝑀 ) )