Theorem cvmsiota

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

	Ref	Expression
Hypotheses	cvmcov.1	⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
	cvmseu.1	⊢ 𝐵 = ∪ 𝐶
	cvmsiota.2	⊢ 𝑊 = ( ℩ 𝑥 ∈ 𝑇 𝐴 ∈ 𝑥 )
Assertion	cvmsiota	⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) → ( 𝑊 ∈ 𝑇 ∧ 𝐴 ∈ 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		cvmcov.1	⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
2		cvmseu.1	⊢ 𝐵 = ∪ 𝐶
3		cvmsiota.2	⊢ 𝑊 = ( ℩ 𝑥 ∈ 𝑇 𝐴 ∈ 𝑥 )
4	1 2	cvmseu	⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) → ∃! 𝑥 ∈ 𝑇 𝐴 ∈ 𝑥 )
5		riotacl2	⊢ ( ∃! 𝑥 ∈ 𝑇 𝐴 ∈ 𝑥 → ( ℩ 𝑥 ∈ 𝑇 𝐴 ∈ 𝑥 ) ∈ { 𝑥 ∈ 𝑇 ∣ 𝐴 ∈ 𝑥 } )
6	4 5	syl	⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) → ( ℩ 𝑥 ∈ 𝑇 𝐴 ∈ 𝑥 ) ∈ { 𝑥 ∈ 𝑇 ∣ 𝐴 ∈ 𝑥 } )
7	3 6	eqeltrid	⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) → 𝑊 ∈ { 𝑥 ∈ 𝑇 ∣ 𝐴 ∈ 𝑥 } )
8		eleq2	⊢ ( 𝑣 = 𝑊 → ( 𝐴 ∈ 𝑣 ↔ 𝐴 ∈ 𝑊 ) )
9		eleq2	⊢ ( 𝑥 = 𝑣 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑣 ) )
10	9	cbvrabv	⊢ { 𝑥 ∈ 𝑇 ∣ 𝐴 ∈ 𝑥 } = { 𝑣 ∈ 𝑇 ∣ 𝐴 ∈ 𝑣 }
11	8 10	elrab2	⊢ ( 𝑊 ∈ { 𝑥 ∈ 𝑇 ∣ 𝐴 ∈ 𝑥 } ↔ ( 𝑊 ∈ 𝑇 ∧ 𝐴 ∈ 𝑊 ) )
12	7 11	sylib	⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑈 ) ) → ( 𝑊 ∈ 𝑇 ∧ 𝐴 ∈ 𝑊 ) )