Metamath Proof Explorer

Theorem cvmliftiota

Description: Write out a function H that is the unique lift of F . (Contributed by Mario Carneiro, 16-Feb-2015)

Ref Expression
Hypotheses cvmliftiota.b ⊢ 𝐵 = ∪ 𝐶
cvmliftiota.h ⊢ 𝐻 = ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
cvmliftiota.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
cvmliftiota.g ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
cvmliftiota.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
cvmliftiota.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
Assertion cvmliftiota ( 𝜑 → ( 𝐻 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐻 ) = 𝐺 ∧ ( 𝐻 ‘ 0 ) = 𝑃 ) )

Proof

Step Hyp Ref Expression
1 cvmliftiota.b ⊢ 𝐵 = ∪ 𝐶
2 cvmliftiota.h ⊢ 𝐻 = ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
3 cvmliftiota.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
4 cvmliftiota.g ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
5 cvmliftiota.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
6 cvmliftiota.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
7 coeq2 ⊢ ( 𝑓 = 𝑔 → ( 𝐹 ∘ 𝑓 ) = ( 𝐹 ∘ 𝑔 ) )
8 7 eqeq1d ⊢ ( 𝑓 = 𝑔 → ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ↔ ( 𝐹 ∘ 𝑔 ) = 𝐺 ) )
9 fveq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ‘ 0 ) = ( 𝑔 ‘ 0 ) )
10 9 eqeq1d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 ‘ 0 ) = 𝑃 ↔ ( 𝑔 ‘ 0 ) = 𝑃 ) )
11 8 10 anbi12d ⊢ ( 𝑓 = 𝑔 → ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) )
12 11 cbvriotavw ⊢ ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) )
13 2 12 eqtri ⊢ 𝐻 = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) )
14 1 cvmlift ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑃 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) ) ) → ∃! 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) )
15 3 4 5 6 14 syl22anc ⊢ ( 𝜑 → ∃! 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) )
16 riotacl2 ⊢ ( ∃! 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ∈ { 𝑔 ∈ ( II Cn 𝐶 ) ∣ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) } )
17 15 16 syl ⊢ ( 𝜑 → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ∈ { 𝑔 ∈ ( II Cn 𝐶 ) ∣ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) } )
18 13 17 eqeltrid ⊢ ( 𝜑 → 𝐻 ∈ { 𝑔 ∈ ( II Cn 𝐶 ) ∣ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) } )
19 coeq2 ⊢ ( 𝑔 = 𝐻 → ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ 𝐻 ) )
20 19 eqeq1d ⊢ ( 𝑔 = 𝐻 → ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ↔ ( 𝐹 ∘ 𝐻 ) = 𝐺 ) )
21 fveq1 ⊢ ( 𝑔 = 𝐻 → ( 𝑔 ‘ 0 ) = ( 𝐻 ‘ 0 ) )
22 21 eqeq1d ⊢ ( 𝑔 = 𝐻 → ( ( 𝑔 ‘ 0 ) = 𝑃 ↔ ( 𝐻 ‘ 0 ) = 𝑃 ) )
23 20 22 anbi12d ⊢ ( 𝑔 = 𝐻 → ( ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ 𝐻 ) = 𝐺 ∧ ( 𝐻 ‘ 0 ) = 𝑃 ) ) )
24 23 elrab ⊢ ( 𝐻 ∈ { 𝑔 ∈ ( II Cn 𝐶 ) ∣ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) } ↔ ( 𝐻 ∈ ( II Cn 𝐶 ) ∧ ( ( 𝐹 ∘ 𝐻 ) = 𝐺 ∧ ( 𝐻 ‘ 0 ) = 𝑃 ) ) )
25 3anass ⊢ ( ( 𝐻 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐻 ) = 𝐺 ∧ ( 𝐻 ‘ 0 ) = 𝑃 ) ↔ ( 𝐻 ∈ ( II Cn 𝐶 ) ∧ ( ( 𝐹 ∘ 𝐻 ) = 𝐺 ∧ ( 𝐻 ‘ 0 ) = 𝑃 ) ) )
26 24 25 bitr4i ⊢ ( 𝐻 ∈ { 𝑔 ∈ ( II Cn 𝐶 ) ∣ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) } ↔ ( 𝐻 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐻 ) = 𝐺 ∧ ( 𝐻 ‘ 0 ) = 𝑃 ) )
27 18 26 sylib ⊢ ( 𝜑 → ( 𝐻 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐻 ) = 𝐺 ∧ ( 𝐻 ‘ 0 ) = 𝑃 ) )