Metamath Proof Explorer

Theorem cvmsiota

Description: Identify the unique element of T containing A . (Contributed by Mario Carneiro, 14-Feb-2015)

Ref Expression
Hypotheses cvmcov.1 ⊢ S = k ∈ J ⟼ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k
cvmseu.1 ⊢ B = ⋃ C
cvmsiota.2 ⊢ W = ι x ∈ T | A ∈ x
Assertion cvmsiota ⊢ F ∈ C CovMap J ∧ T ∈ S ⁡ U ∧ A ∈ B ∧ F ⁡ A ∈ U → W ∈ T ∧ A ∈ W

Proof

Step Hyp Ref Expression
1 cvmcov.1 ⊢ S = k ∈ J ⟼ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k
2 cvmseu.1 ⊢ B = ⋃ C
3 cvmsiota.2 ⊢ W = ι x ∈ T | A ∈ x
4 1 2 cvmseu ⊢ F ∈ C CovMap J ∧ T ∈ S ⁡ U ∧ A ∈ B ∧ F ⁡ A ∈ U → ∃! x ∈ T A ∈ x
5 riotacl2 ⊢ ∃! x ∈ T A ∈ x → ι x ∈ T | A ∈ x ∈ x ∈ T | A ∈ x
6 4 5 syl ⊢ F ∈ C CovMap J ∧ T ∈ S ⁡ U ∧ A ∈ B ∧ F ⁡ A ∈ U → ι x ∈ T | A ∈ x ∈ x ∈ T | A ∈ x
7 3 6 eqeltrid ⊢ F ∈ C CovMap J ∧ T ∈ S ⁡ U ∧ A ∈ B ∧ F ⁡ A ∈ U → W ∈ x ∈ T | A ∈ x
8 eleq2 ⊢ v = W → A ∈ v ↔ A ∈ W
9 eleq2 ⊢ x = v → A ∈ x ↔ A ∈ v
10 9 cbvrabv ⊢ x ∈ T | A ∈ x = v ∈ T | A ∈ v
11 8 10 elrab2 ⊢ W ∈ x ∈ T | A ∈ x ↔ W ∈ T ∧ A ∈ W
12 7 11 sylib ⊢ F ∈ C CovMap J ∧ T ∈ S ⁡ U ∧ A ∈ B ∧ F ⁡ A ∈ U → W ∈ T ∧ A ∈ W