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 imbitrrdi ⊢ ( ∀ 𝑦 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑦 } ) ( ( 𝑢 × { 𝑥 } ) ⊆ 𝑀 ↔ ( 𝑢 × { 𝑡 } ) ⊆ 𝑀 ) → ( ( ( 0 [,] 1 ) × { 𝑥 } ) ⊆ 𝑀 → ( ( 0 [,] 1 ) × { 𝑡 } ) ⊆ 𝑀 ) )