Theorem cvmlift3lem9 33298

Description: Lemma for cvmlift2 33287. (Contributed by Mario Carneiro, 7-May-2015.)

Hypotheses

Ref	Expression
cvmlift3.b	⊢ 𝐵 = ∪ 𝐶
cvmlift3.y	⊢ 𝑌 = ∪ 𝐾
cvmlift3.f	⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))
cvmlift3.k	⊢ (𝜑 → 𝐾 ∈ SConn)
cvmlift3.l	⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn)
cvmlift3.o	⊢ (𝜑 → 𝑂 ∈ 𝑌)
cvmlift3.g	⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))
cvmlift3.p	⊢ (𝜑 → 𝑃 ∈ 𝐵)
cvmlift3.e	⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂))
cvmlift3.h	⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧)))
cvmlift3lem7.s	⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))})

Assertion

Ref	Expression
cvmlift3lem9	⊢ (𝜑 → ∃𝑓 ∈ (𝐾 Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘𝑂) = 𝑃))

Distinct variable groups:   𝑐,𝑑,𝑓,𝑘,𝑠,𝑧,𝑔,𝑥   𝐽,𝑐   𝑔,𝑑,𝑥,𝐽,𝑓,𝑘,𝑠   𝐹,𝑐,𝑑,𝑓,𝑔,𝑘,𝑠   𝑥,𝑧,𝐹   𝐻,𝑐,𝑑,𝑓,𝑔,𝑥,𝑧   𝑆,𝑓,𝑥   𝐵,𝑑,𝑓,𝑔,𝑥,𝑧   𝐺,𝑐,𝑑,𝑓,𝑔,𝑘,𝑥,𝑧   𝐶,𝑐,𝑑,𝑓,𝑔,𝑘,𝑠,𝑥,𝑧   𝜑,𝑓,𝑥   𝐾,𝑐,𝑓,𝑔,𝑥,𝑧   𝑃,𝑐,𝑑,𝑓,𝑔,𝑥,𝑧   𝑂,𝑐,𝑓,𝑔,𝑥,𝑧   𝑓,𝑌,𝑔,𝑥,𝑧

Allowed substitution hints:   𝜑(𝑧,𝑔,𝑘,𝑠,𝑐,𝑑)   𝐵(𝑘,𝑠,𝑐)   𝑃(𝑘,𝑠)   𝑆(𝑧,𝑔,𝑘,𝑠,𝑐,𝑑)   𝐺(𝑠)   𝐻(𝑘,𝑠)   𝐽(𝑧)   𝐾(𝑘,𝑠,𝑑)   𝑂(𝑘,𝑠,𝑑)   𝑌(𝑘,𝑠,𝑐,𝑑)

Proof of Theorem cvmlift3lem9

Step	Hyp	Ref	Expression
1		cvmlift3.b	. . 3 ⊢ 𝐵 = ∪ 𝐶
2		cvmlift3.y	. . 3 ⊢ 𝑌 = ∪ 𝐾
3		cvmlift3.f	. . 3 ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))
4		cvmlift3.k	. . 3 ⊢ (𝜑 → 𝐾 ∈ SConn)
5		cvmlift3.l	. . 3 ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn)
6		cvmlift3.o	. . 3 ⊢ (𝜑 → 𝑂 ∈ 𝑌)
7		cvmlift3.g	. . 3 ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))
8		cvmlift3.p	. . 3 ⊢ (𝜑 → 𝑃 ∈ 𝐵)
9		cvmlift3.e	. . 3 ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂))
10		cvmlift3.h	. . 3 ⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧)))
11		cvmlift3lem7.s	. . 3 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))})
12	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11	cvmlift3lem8 33297	. 2 ⊢ (𝜑 → 𝐻 ∈ (𝐾 Cn 𝐶))
13	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	cvmlift3lem5 33294	. 2 ⊢ (𝜑 → (𝐹 ∘ 𝐻) = 𝐺)
14		iitopon 24051	. . . . . 6 ⊢ II ∈ (TopOn‘(0[,]1))
15	14	a1i 11	. . . . 5 ⊢ (𝜑 → II ∈ (TopOn‘(0[,]1)))
16		sconntop 33199	. . . . . . 7 ⊢ (𝐾 ∈ SConn → 𝐾 ∈ Top)
17	4, 16	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ Top)
18	2	toptopon 22075	. . . . . 6 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌))
19	17, 18	sylib 217	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))
20		cnconst2 22443	. . . . 5 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑂 ∈ 𝑌) → ((0[,]1) × {𝑂}) ∈ (II Cn 𝐾))
21	15, 19, 6, 20	syl3anc 1370	. . . 4 ⊢ (𝜑 → ((0[,]1) × {𝑂}) ∈ (II Cn 𝐾))
22		0elunit 13210	. . . . 5 ⊢ 0 ∈ (0[,]1)
23		fvconst2g 7086	. . . . 5 ⊢ ((𝑂 ∈ 𝑌 ∧ 0 ∈ (0[,]1)) → (((0[,]1) × {𝑂})‘0) = 𝑂)
24	6, 22, 23	sylancl 586	. . . 4 ⊢ (𝜑 → (((0[,]1) × {𝑂})‘0) = 𝑂)
25		1elunit 13211	. . . . 5 ⊢ 1 ∈ (0[,]1)
26		fvconst2g 7086	. . . . 5 ⊢ ((𝑂 ∈ 𝑌 ∧ 1 ∈ (0[,]1)) → (((0[,]1) × {𝑂})‘1) = 𝑂)
27	6, 25, 26	sylancl 586	. . . 4 ⊢ (𝜑 → (((0[,]1) × {𝑂})‘1) = 𝑂)
28	9	sneqd 4574	. . . . . . . . 9 ⊢ (𝜑 → {(𝐹‘𝑃)} = {(𝐺‘𝑂)})
29	28	xpeq2d 5620	. . . . . . . 8 ⊢ (𝜑 → ((0[,]1) × {(𝐹‘𝑃)}) = ((0[,]1) × {(𝐺‘𝑂)}))
30		cvmcn 33233	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
31		eqid 2739	. . . . . . . . . . 11 ⊢ ∪ 𝐽 = ∪ 𝐽
32	1, 31	cnf 22406	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽)
33		ffn 6609	. . . . . . . . . 10 ⊢ (𝐹:𝐵⟶∪ 𝐽 → 𝐹 Fn 𝐵)
34	3, 30, 32, 33	4syl 19	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝐵)
35		fcoconst 7015	. . . . . . . . 9 ⊢ ((𝐹 Fn 𝐵 ∧ 𝑃 ∈ 𝐵) → (𝐹 ∘ ((0[,]1) × {𝑃})) = ((0[,]1) × {(𝐹‘𝑃)}))
36	34, 8, 35	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∘ ((0[,]1) × {𝑃})) = ((0[,]1) × {(𝐹‘𝑃)}))
37	2, 31	cnf 22406	. . . . . . . . . . 11 ⊢ (𝐺 ∈ (𝐾 Cn 𝐽) → 𝐺:𝑌⟶∪ 𝐽)
38	7, 37	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:𝑌⟶∪ 𝐽)
39	38	ffnd 6610	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 Fn 𝑌)
40		fcoconst 7015	. . . . . . . . 9 ⊢ ((𝐺 Fn 𝑌 ∧ 𝑂 ∈ 𝑌) → (𝐺 ∘ ((0[,]1) × {𝑂})) = ((0[,]1) × {(𝐺‘𝑂)}))
41	39, 6, 40	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝐺 ∘ ((0[,]1) × {𝑂})) = ((0[,]1) × {(𝐺‘𝑂)}))
42	29, 36, 41	3eqtr4d 2789	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∘ ((0[,]1) × {𝑃})) = (𝐺 ∘ ((0[,]1) × {𝑂})))
43		fvconst2g 7086	. . . . . . . 8 ⊢ ((𝑃 ∈ 𝐵 ∧ 0 ∈ (0[,]1)) → (((0[,]1) × {𝑃})‘0) = 𝑃)
44	8, 22, 43	sylancl 586	. . . . . . 7 ⊢ (𝜑 → (((0[,]1) × {𝑃})‘0) = 𝑃)
45		cvmtop1 33231	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
46	3, 45	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ Top)
47	1	toptopon 22075	. . . . . . . . . 10 ⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
48	46, 47	sylib 217	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵))
49		cnconst2 22443	. . . . . . . . 9 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ 𝐶 ∈ (TopOn‘𝐵) ∧ 𝑃 ∈ 𝐵) → ((0[,]1) × {𝑃}) ∈ (II Cn 𝐶))
50	15, 48, 8, 49	syl3anc 1370	. . . . . . . 8 ⊢ (𝜑 → ((0[,]1) × {𝑃}) ∈ (II Cn 𝐶))
51		cvmtop2 33232	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top)
52	3, 51	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ Top)
53	31	toptopon 22075	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))
54	52, 53	sylib 217	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽))
55	38, 6	ffvelrnd 6971	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺‘𝑂) ∈ ∪ 𝐽)
56		cnconst2 22443	. . . . . . . . . . 11 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ 𝐽 ∈ (TopOn‘∪ 𝐽) ∧ (𝐺‘𝑂) ∈ ∪ 𝐽) → ((0[,]1) × {(𝐺‘𝑂)}) ∈ (II Cn 𝐽))
57	15, 54, 55, 56	syl3anc 1370	. . . . . . . . . 10 ⊢ (𝜑 → ((0[,]1) × {(𝐺‘𝑂)}) ∈ (II Cn 𝐽))
58	41, 57	eqeltrd 2840	. . . . . . . . 9 ⊢ (𝜑 → (𝐺 ∘ ((0[,]1) × {𝑂})) ∈ (II Cn 𝐽))
59		fvconst2g 7086	. . . . . . . . . . 11 ⊢ (((𝐺‘𝑂) ∈ ∪ 𝐽 ∧ 0 ∈ (0[,]1)) → (((0[,]1) × {(𝐺‘𝑂)})‘0) = (𝐺‘𝑂))
60	55, 22, 59	sylancl 586	. . . . . . . . . 10 ⊢ (𝜑 → (((0[,]1) × {(𝐺‘𝑂)})‘0) = (𝐺‘𝑂))
61	41	fveq1d 6785	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐺 ∘ ((0[,]1) × {𝑂}))‘0) = (((0[,]1) × {(𝐺‘𝑂)})‘0))
62	60, 61, 9	3eqtr4rd 2790	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘𝑃) = ((𝐺 ∘ ((0[,]1) × {𝑂}))‘0))
63	1	cvmlift 33270	. . . . . . . . 9 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐺 ∘ ((0[,]1) × {𝑂})) ∈ (II Cn 𝐽)) ∧ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = ((𝐺 ∘ ((0[,]1) × {𝑂}))‘0))) → ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))
64	3, 58, 8, 62, 63	syl22anc 836	. . . . . . . 8 ⊢ (𝜑 → ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))
65		coeq2 5770	. . . . . . . . . . 11 ⊢ (𝑔 = ((0[,]1) × {𝑃}) → (𝐹 ∘ 𝑔) = (𝐹 ∘ ((0[,]1) × {𝑃})))
66	65	eqeq1d 2741	. . . . . . . . . 10 ⊢ (𝑔 = ((0[,]1) × {𝑃}) → ((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ↔ (𝐹 ∘ ((0[,]1) × {𝑃})) = (𝐺 ∘ ((0[,]1) × {𝑂}))))
67		fveq1 6782	. . . . . . . . . . 11 ⊢ (𝑔 = ((0[,]1) × {𝑃}) → (𝑔‘0) = (((0[,]1) × {𝑃})‘0))
68	67	eqeq1d 2741	. . . . . . . . . 10 ⊢ (𝑔 = ((0[,]1) × {𝑃}) → ((𝑔‘0) = 𝑃 ↔ (((0[,]1) × {𝑃})‘0) = 𝑃))
69	66, 68	anbi12d 631	. . . . . . . . 9 ⊢ (𝑔 = ((0[,]1) × {𝑃}) → (((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹 ∘ ((0[,]1) × {𝑃})) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (((0[,]1) × {𝑃})‘0) = 𝑃)))
70	69	riota2 7267	. . . . . . . 8 ⊢ ((((0[,]1) × {𝑃}) ∈ (II Cn 𝐶) ∧ ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)) → (((𝐹 ∘ ((0[,]1) × {𝑃})) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (((0[,]1) × {𝑃})‘0) = 𝑃) ↔ (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)) = ((0[,]1) × {𝑃})))
71	50, 64, 70	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (((𝐹 ∘ ((0[,]1) × {𝑃})) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (((0[,]1) × {𝑃})‘0) = 𝑃) ↔ (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)) = ((0[,]1) × {𝑃})))
72	42, 44, 71	mpbi2and 709	. . . . . 6 ⊢ (𝜑 → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)) = ((0[,]1) × {𝑃}))
73	72	fveq1d 6785	. . . . 5 ⊢ (𝜑 → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1) = (((0[,]1) × {𝑃})‘1))
74		fvconst2g 7086	. . . . . 6 ⊢ ((𝑃 ∈ 𝐵 ∧ 1 ∈ (0[,]1)) → (((0[,]1) × {𝑃})‘1) = 𝑃)
75	8, 25, 74	sylancl 586	. . . . 5 ⊢ (𝜑 → (((0[,]1) × {𝑃})‘1) = 𝑃)
76	73, 75	eqtrd 2779	. . . 4 ⊢ (𝜑 → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃)
77		fveq1 6782	. . . . . . 7 ⊢ (𝑓 = ((0[,]1) × {𝑂}) → (𝑓‘0) = (((0[,]1) × {𝑂})‘0))
78	77	eqeq1d 2741	. . . . . 6 ⊢ (𝑓 = ((0[,]1) × {𝑂}) → ((𝑓‘0) = 𝑂 ↔ (((0[,]1) × {𝑂})‘0) = 𝑂))
79		fveq1 6782	. . . . . . 7 ⊢ (𝑓 = ((0[,]1) × {𝑂}) → (𝑓‘1) = (((0[,]1) × {𝑂})‘1))
80	79	eqeq1d 2741	. . . . . 6 ⊢ (𝑓 = ((0[,]1) × {𝑂}) → ((𝑓‘1) = 𝑂 ↔ (((0[,]1) × {𝑂})‘1) = 𝑂))
81		coeq2 5770	. . . . . . . . . . 11 ⊢ (𝑓 = ((0[,]1) × {𝑂}) → (𝐺 ∘ 𝑓) = (𝐺 ∘ ((0[,]1) × {𝑂})))
82	81	eqeq2d 2750	. . . . . . . . . 10 ⊢ (𝑓 = ((0[,]1) × {𝑂}) → ((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ↔ (𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂}))))
83	82	anbi1d 630	. . . . . . . . 9 ⊢ (𝑓 = ((0[,]1) × {𝑂}) → (((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)))
84	83	riotabidv 7243	. . . . . . . 8 ⊢ (𝑓 = ((0[,]1) × {𝑂}) → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)) = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃)))
85	84	fveq1d 6785	. . . . . . 7 ⊢ (𝑓 = ((0[,]1) × {𝑂}) → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1))
86	85	eqeq1d 2741	. . . . . 6 ⊢ (𝑓 = ((0[,]1) × {𝑂}) → (((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃 ↔ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃))
87	78, 80, 86	3anbi123d 1435	. . . . 5 ⊢ (𝑓 = ((0[,]1) × {𝑂}) → (((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃) ↔ ((((0[,]1) × {𝑂})‘0) = 𝑂 ∧ (((0[,]1) × {𝑂})‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃)))
88	87	rspcev 3562	. . . 4 ⊢ ((((0[,]1) × {𝑂}) ∈ (II Cn 𝐾) ∧ ((((0[,]1) × {𝑂})‘0) = 𝑂 ∧ (((0[,]1) × {𝑂})‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ ((0[,]1) × {𝑂})) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃)) → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃))
89	21, 24, 27, 76, 88	syl13anc 1371	. . 3 ⊢ (𝜑 → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃))
90	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	cvmlift3lem4 33293	. . . 4 ⊢ ((𝜑 ∧ 𝑂 ∈ 𝑌) → ((𝐻‘𝑂) = 𝑃 ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃)))
91	6, 90	mpdan 684	. . 3 ⊢ (𝜑 → ((𝐻‘𝑂) = 𝑃 ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑂 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑃)))
92	89, 91	mpbird 256	. 2 ⊢ (𝜑 → (𝐻‘𝑂) = 𝑃)
93		coeq2 5770	. . . . 5 ⊢ (𝑓 = 𝐻 → (𝐹 ∘ 𝑓) = (𝐹 ∘ 𝐻))
94	93	eqeq1d 2741	. . . 4 ⊢ (𝑓 = 𝐻 → ((𝐹 ∘ 𝑓) = 𝐺 ↔ (𝐹 ∘ 𝐻) = 𝐺))
95		fveq1 6782	. . . . 5 ⊢ (𝑓 = 𝐻 → (𝑓‘𝑂) = (𝐻‘𝑂))
96	95	eqeq1d 2741	. . . 4 ⊢ (𝑓 = 𝐻 → ((𝑓‘𝑂) = 𝑃 ↔ (𝐻‘𝑂) = 𝑃))
97	94, 96	anbi12d 631	. . 3 ⊢ (𝑓 = 𝐻 → (((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘𝑂) = 𝑃) ↔ ((𝐹 ∘ 𝐻) = 𝐺 ∧ (𝐻‘𝑂) = 𝑃)))
98	97	rspcev 3562	. 2 ⊢ ((𝐻 ∈ (𝐾 Cn 𝐶) ∧ ((𝐹 ∘ 𝐻) = 𝐺 ∧ (𝐻‘𝑂) = 𝑃)) → ∃𝑓 ∈ (𝐾 Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘𝑂) = 𝑃))
99	12, 13, 92, 98	syl12anc 834	1 ⊢ (𝜑 → ∃𝑓 ∈ (𝐾 Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘𝑂) = 𝑃))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  ∀wral 3065  ∃wrex 3066  ∃!wreu 3067  {crab 3069   ∖ cdif 3885   ∩ cin 3887  ∅c0 4257  𝒫 cpw 4534  {csn 4562  ∪ cuni 4840   ↦ cmpt 5158   × cxp 5588  ^◡ccnv 5589   ↾ cres 5592   “ cima 5593   ∘ ccom 5594   Fn wfn 6432  ⟶wf 6433  ‘cfv 6437  ℩crio 7240  (class class class)co 7284  0cc0 10880  1c1 10881  [,]cicc 13091   ↾_t crest 17140  Topctop 22051  TopOnctopon 22068   Cn ccn 22384  𝑛-Locally cnlly 22625  Homeochmeo 22913  IIcii 24047  PConncpconn 33190  SConncsconn 33191   CovMap ccvm 33226

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-inf2 9408  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957  ax-pre-sup 10958  ax-addf 10959  ax-mulf 10960

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-iin 4928  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-se 5546  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-isom 6446  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-of 7542  df-om 7722  df-1st 7840  df-2nd 7841  df-supp 7987  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-2o 8307  df-er 8507  df-ec 8509  df-map 8626  df-ixp 8695  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-fsupp 9138  df-fi 9179  df-sup 9210  df-inf 9211  df-oi 9278  df-card 9706  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-div 11642  df-nn 11983  df-2 12045  df-3 12046  df-4 12047  df-5 12048  df-6 12049  df-7 12050  df-8 12051  df-9 12052  df-n0 12243  df-z 12329  df-dec 12447  df-uz 12592  df-q 12698  df-rp 12740  df-xneg 12857  df-xadd 12858  df-xmul 12859  df-ioo 13092  df-ico 13094  df-icc 13095  df-fz 13249  df-fzo 13392  df-fl 13521  df-seq 13731  df-exp 13792  df-hash 14054  df-cj 14819  df-re 14820  df-im 14821  df-sqrt 14955  df-abs 14956  df-clim 15206  df-sum 15407  df-struct 16857  df-sets 16874  df-slot 16892  df-ndx 16904  df-base 16922  df-ress 16951  df-plusg 16984  df-mulr 16985  df-starv 16986  df-sca 16987  df-vsca 16988  df-ip 16989  df-tset 16990  df-ple 16991  df-ds 16993  df-unif 16994  df-hom 16995  df-cco 16996  df-rest 17142  df-topn 17143  df-0g 17161  df-gsum 17162  df-topgen 17163  df-pt 17164  df-prds 17167  df-xrs 17222  df-qtop 17227  df-imas 17228  df-xps 17230  df-mre 17304  df-mrc 17305  df-acs 17307  df-mgm 18335  df-sgrp 18384  df-mnd 18395  df-submnd 18440  df-mulg 18710  df-cntz 18932  df-cmn 19397  df-psmet 20598  df-xmet 20599  df-met 20600  df-bl 20601  df-mopn 20602  df-cnfld 20607  df-top 22052  df-topon 22069  df-topsp 22091  df-bases 22105  df-cld 22179  df-ntr 22180  df-cls 22181  df-nei 22258  df-cn 22387  df-cnp 22388  df-cmp 22547  df-conn 22572  df-lly 22626  df-nlly 22627  df-tx 22722  df-hmeo 22915  df-xms 23482  df-ms 23483  df-tms 23484  df-ii 24049  df-htpy 24142  df-phtpy 24143  df-phtpc 24164  df-pco 24177  df-pconn 33192  df-sconn 33193  df-cvm 33227

This theorem is referenced by:  cvmlift3  33299