Metamath Proof Explorer

Theorem cvmsi

Description: One direction of cvmsval . (Contributed by Mario Carneiro, 13-Feb-2015)

Ref Expression
Hypothesis cvmcov.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
Assertion cvmsi ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → ( 𝑈 ∈ 𝐽 ∧ ( 𝑇 ⊆ 𝐶 ∧ 𝑇 ≠ ∅ ) ∧ ( ∪ 𝑇 = ( ◡ 𝐹 “ 𝑈 ) ∧ ∀ 𝑢 ∈ 𝑇 ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cvmcov.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
2 1 cvmsrcl ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → 𝑈 ∈ 𝐽 )
3 imaeq2 ⊢ ( 𝑘 = 𝑈 → ( ◡ 𝐹 “ 𝑘 ) = ( ◡ 𝐹 “ 𝑈 ) )
4 3 eqeq2d ⊢ ( 𝑘 = 𝑈 → ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ↔ ∪ 𝑠 = ( ◡ 𝐹 “ 𝑈 ) ) )
5 oveq2 ⊢ ( 𝑘 = 𝑈 → ( 𝐽 ↾t 𝑘 ) = ( 𝐽 ↾t 𝑈 ) )
6 5 oveq2d ⊢ ( 𝑘 = 𝑈 → ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) = ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) )
7 6 eleq2d ⊢ ( 𝑘 = 𝑈 → ( ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ↔ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) )
8 7 anbi2d ⊢ ( 𝑘 = 𝑈 → ( ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ↔ ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) )
9 8 ralbidv ⊢ ( 𝑘 = 𝑈 → ( ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ↔ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) )
10 4 9 anbi12d ⊢ ( 𝑘 = 𝑈 → ( ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ↔ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑈 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) ) )
11 10 rabbidv ⊢ ( 𝑘 = 𝑈 → { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } = { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑈 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) } )
12 11 1 fvmptss2 ⊢ ( 𝑆 ‘ 𝑈 ) ⊆ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑈 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) }
13 12 sseli ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → 𝑇 ∈ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑈 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) } )
14 unieq ⊢ ( 𝑠 = 𝑇 → ∪ 𝑠 = ∪ 𝑇 )
15 14 eqeq1d ⊢ ( 𝑠 = 𝑇 → ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑈 ) ↔ ∪ 𝑇 = ( ◡ 𝐹 “ 𝑈 ) ) )
16 difeq1 ⊢ ( 𝑠 = 𝑇 → ( 𝑠 ∖ { 𝑢 } ) = ( 𝑇 ∖ { 𝑢 } ) )
17 16 raleqdv ⊢ ( 𝑠 = 𝑇 → ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ↔ ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) )
18 17 anbi1d ⊢ ( 𝑠 = 𝑇 → ( ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ↔ ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) )
19 18 raleqbi1dv ⊢ ( 𝑠 = 𝑇 → ( ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ↔ ∀ 𝑢 ∈ 𝑇 ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) )
20 15 19 anbi12d ⊢ ( 𝑠 = 𝑇 → ( ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑈 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) ↔ ( ∪ 𝑇 = ( ◡ 𝐹 “ 𝑈 ) ∧ ∀ 𝑢 ∈ 𝑇 ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) ) )
21 20 elrab ⊢ ( 𝑇 ∈ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑈 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) } ↔ ( 𝑇 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∧ ( ∪ 𝑇 = ( ◡ 𝐹 “ 𝑈 ) ∧ ∀ 𝑢 ∈ 𝑇 ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) ) )
22 13 21 sylib ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → ( 𝑇 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∧ ( ∪ 𝑇 = ( ◡ 𝐹 “ 𝑈 ) ∧ ∀ 𝑢 ∈ 𝑇 ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) ) )
23 22 simpld ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → 𝑇 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) )
24 eldifsn ⊢ ( 𝑇 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ↔ ( 𝑇 ∈ 𝒫 𝐶 ∧ 𝑇 ≠ ∅ ) )
25 23 24 sylib ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → ( 𝑇 ∈ 𝒫 𝐶 ∧ 𝑇 ≠ ∅ ) )
26 elpwi ⊢ ( 𝑇 ∈ 𝒫 𝐶 → 𝑇 ⊆ 𝐶 )
27 26 anim1i ⊢ ( ( 𝑇 ∈ 𝒫 𝐶 ∧ 𝑇 ≠ ∅ ) → ( 𝑇 ⊆ 𝐶 ∧ 𝑇 ≠ ∅ ) )
28 25 27 syl ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → ( 𝑇 ⊆ 𝐶 ∧ 𝑇 ≠ ∅ ) )
29 22 simprd ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → ( ∪ 𝑇 = ( ◡ 𝐹 “ 𝑈 ) ∧ ∀ 𝑢 ∈ 𝑇 ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) )
30 2 28 29 3jca ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → ( 𝑈 ∈ 𝐽 ∧ ( 𝑇 ⊆ 𝐶 ∧ 𝑇 ≠ ∅ ) ∧ ( ∪ 𝑇 = ( ◡ 𝐹 “ 𝑈 ) ∧ ∀ 𝑢 ∈ 𝑇 ( ∀ 𝑣 ∈ ( 𝑇 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) ) ) )