ptpjopn

Description: The projection map is an open map. (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	ptpjcn.1	$⊢ Y = ⋃ J$
	ptpjcn.2	$⊢ J = \prod_{𝑡} (F)$
Assertion	ptpjopn	$⊢ ((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \to (x \in Y ⟼ x (I)) [U] \in F (I)$

Proof

Step	Hyp	Ref	Expression
1		ptpjcn.1	$⊢ Y = ⋃ J$
2		ptpjcn.2	$⊢ J = \prod_{𝑡} (F)$
3		df-ima	$⊢ (x \in Y ⟼ x (I)) [U] = ran ({(x \in Y ⟼ x (I)) ↾}_{U})$
4		elssuni	$⊢ U \in J \to U \subseteq ⋃ J$
5	4 1	sseqtrrdi	$⊢ U \in J \to U \subseteq Y$
6	5	adantl	$⊢ ((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \to U \subseteq Y$
7	6	resmptd	$⊢ ((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \to {(x \in Y ⟼ x (I)) ↾}_{U} = (x \in U ⟼ x (I))$
8	7	rneqd	$⊢ ((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \to ran ({(x \in Y ⟼ x (I)) ↾}_{U}) = ran (x \in U ⟼ x (I))$
9	3 8	eqtrid	$⊢ ((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \to (x \in Y ⟼ x (I)) [U] = ran (x \in U ⟼ x (I))$
10		ffn	$⊢ F : A ⟶ Top \to F Fn A$
11		eqid	$⊢ \{s \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land s = \underset{y \in A}{⨉} g (y))\} = \{s \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land s = \underset{y \in A}{⨉} g (y))\}$
12	11	ptval	$⊢ (A \in V \land F Fn A) \to \prod_{𝑡} (F) = topGen (\{s \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land s = \underset{y \in A}{⨉} g (y))\})$
13	10 12	sylan2	$⊢ (A \in V \land F : A ⟶ Top) \to \prod_{𝑡} (F) = topGen (\{s \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land s = \underset{y \in A}{⨉} g (y))\})$
14	2 13	eqtrid	$⊢ (A \in V \land F : A ⟶ Top) \to J = topGen (\{s \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land s = \underset{y \in A}{⨉} g (y))\})$
15	14	3adant3	$⊢ (A \in V \land F : A ⟶ Top \land I \in A) \to J = topGen (\{s \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land s = \underset{y \in A}{⨉} g (y))\})$
16	15	eleq2d	$⊢ (A \in V \land F : A ⟶ Top \land I \in A) \to (U \in J \leftrightarrow U \in topGen (\{s \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land s = \underset{y \in A}{⨉} g (y))\}))$
17	16	biimpa	$⊢ ((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \to U \in topGen (\{s \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land s = \underset{y \in A}{⨉} g (y))\})$
18		tg2	$⊢ (U \in topGen (\{s \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land s = \underset{y \in A}{⨉} g (y))\}) \land s \in U) \to \exists w \in \{s \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land s = \underset{y \in A}{⨉} g (y))\} (s \in w \land w \subseteq U)$
19	17 18	sylan	$⊢ (((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \to \exists w \in \{s \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land s = \underset{y \in A}{⨉} g (y))\} (s \in w \land w \subseteq U)$
20		vex	$⊢ w \in V$
21		eqeq1	$⊢ s = w \to (s = \underset{y \in A}{⨉} g (y) \leftrightarrow w = \underset{y \in A}{⨉} g (y))$
22	21	anbi2d	$⊢ s = w \to (((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land s = \underset{y \in A}{⨉} g (y)) \leftrightarrow ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land w = \underset{y \in A}{⨉} g (y)))$
23	22	exbidv	$⊢ s = w \to (\exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land s = \underset{y \in A}{⨉} g (y)) \leftrightarrow \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land w = \underset{y \in A}{⨉} g (y)))$
24	20 23	elab	$⊢ w \in \{s \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land s = \underset{y \in A}{⨉} g (y))\} \leftrightarrow \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land w = \underset{y \in A}{⨉} g (y))$
25		fveq2	$⊢ y = I \to g (y) = g (I)$
26		fveq2	$⊢ y = I \to F (y) = F (I)$
27	25 26	eleq12d	$⊢ y = I \to (g (y) \in F (y) \leftrightarrow g (I) \in F (I))$
28		simplr2	$⊢ (((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \to \forall y \in A g (y) \in F (y)$
29		simpl3	$⊢ ((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \to I \in A$
30	29	ad3antrrr	$⊢ (((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \to I \in A$
31	27 28 30	rspcdva	$⊢ (((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \to g (I) \in F (I)$
32		fveq2	$⊢ y = I \to s (y) = s (I)$
33	32 25	eleq12d	$⊢ y = I \to (s (y) \in g (y) \leftrightarrow s (I) \in g (I))$
34		vex	$⊢ s \in V$
35	34	elixp	$⊢ s \in \underset{y \in A}{⨉} g (y) \leftrightarrow (s Fn A \land \forall y \in A s (y) \in g (y))$
36	35	simprbi	$⊢ s \in \underset{y \in A}{⨉} g (y) \to \forall y \in A s (y) \in g (y)$
37	36	ad2antrl	$⊢ (((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \to \forall y \in A s (y) \in g (y)$
38	33 37 30	rspcdva	$⊢ (((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \to s (I) \in g (I)$
39		simplrr	$⊢ ((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land k \in g (I)) \to \underset{y \in A}{⨉} g (y) \subseteq U$
40		simplrl	$⊢ (((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land (k \in g (I) \land n \in A)) \land n = I) \to k \in g (I)$
41		fveq2	$⊢ n = I \to g (n) = g (I)$
42	41	adantl	$⊢ (((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land (k \in g (I) \land n \in A)) \land n = I) \to g (n) = g (I)$
43	40 42	eleqtrrd	$⊢ (((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land (k \in g (I) \land n \in A)) \land n = I) \to k \in g (n)$
44		fveq2	$⊢ y = n \to s (y) = s (n)$
45		fveq2	$⊢ y = n \to g (y) = g (n)$
46	44 45	eleq12d	$⊢ y = n \to (s (y) \in g (y) \leftrightarrow s (n) \in g (n))$
47		simplrl	$⊢ ((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land (k \in g (I) \land n \in A)) \to s \in \underset{y \in A}{⨉} g (y)$
48	47 36	syl	$⊢ ((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land (k \in g (I) \land n \in A)) \to \forall y \in A s (y) \in g (y)$
49		simprr	$⊢ ((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land (k \in g (I) \land n \in A)) \to n \in A$
50	46 48 49	rspcdva	$⊢ ((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land (k \in g (I) \land n \in A)) \to s (n) \in g (n)$
51	50	adantr	$⊢ (((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land (k \in g (I) \land n \in A)) \land \neg n = I) \to s (n) \in g (n)$
52	43 51	ifclda	$⊢ ((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land (k \in g (I) \land n \in A)) \to if (n = I, k, s (n)) \in g (n)$
53	52	anassrs	$⊢ (((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land k \in g (I)) \land n \in A) \to if (n = I, k, s (n)) \in g (n)$
54	53	ralrimiva	$⊢ ((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land k \in g (I)) \to \forall n \in A if (n = I, k, s (n)) \in g (n)$
55		simpll1	$⊢ (((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \to A \in V$
56	55	ad3antrrr	$⊢ ((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land k \in g (I)) \to A \in V$
57		mptelixpg	$⊢ A \in V \to ((n \in A ⟼ if (n = I, k, s (n))) \in \underset{n \in A}{⨉} g (n) \leftrightarrow \forall n \in A if (n = I, k, s (n)) \in g (n))$
58	56 57	syl	$⊢ ((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land k \in g (I)) \to ((n \in A ⟼ if (n = I, k, s (n))) \in \underset{n \in A}{⨉} g (n) \leftrightarrow \forall n \in A if (n = I, k, s (n)) \in g (n))$
59	54 58	mpbird	$⊢ ((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land k \in g (I)) \to (n \in A ⟼ if (n = I, k, s (n))) \in \underset{n \in A}{⨉} g (n)$
60		fveq2	$⊢ n = y \to g (n) = g (y)$
61	60	cbvixpv	$⊢ \underset{n \in A}{⨉} g (n) = \underset{y \in A}{⨉} g (y)$
62	59 61	eleqtrdi	$⊢ ((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land k \in g (I)) \to (n \in A ⟼ if (n = I, k, s (n))) \in \underset{y \in A}{⨉} g (y)$
63	39 62	sseldd	$⊢ ((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land k \in g (I)) \to (n \in A ⟼ if (n = I, k, s (n))) \in U$
64	30	adantr	$⊢ ((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land k \in g (I)) \to I \in A$
65		iftrue	$⊢ n = I \to if (n = I, k, s (n)) = k$
66		eqid	$⊢ (n \in A ⟼ if (n = I, k, s (n))) = (n \in A ⟼ if (n = I, k, s (n)))$
67		vex	$⊢ k \in V$
68	65 66 67	fvmpt	$⊢ I \in A \to (n \in A ⟼ if (n = I, k, s (n))) (I) = k$
69	64 68	syl	$⊢ ((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land k \in g (I)) \to (n \in A ⟼ if (n = I, k, s (n))) (I) = k$
70	69	eqcomd	$⊢ ((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land k \in g (I)) \to k = (n \in A ⟼ if (n = I, k, s (n))) (I)$
71		fveq1	$⊢ x = (n \in A ⟼ if (n = I, k, s (n))) \to x (I) = (n \in A ⟼ if (n = I, k, s (n))) (I)$
72	71	rspceeqv	$⊢ ((n \in A ⟼ if (n = I, k, s (n))) \in U \land k = (n \in A ⟼ if (n = I, k, s (n))) (I)) \to \exists x \in U k = x (I)$
73	63 70 72	syl2anc	$⊢ ((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land k \in g (I)) \to \exists x \in U k = x (I)$
74		eqid	$⊢ (x \in U ⟼ x (I)) = (x \in U ⟼ x (I))$
75	74	elrnmpt	$⊢ k \in V \to (k \in ran (x \in U ⟼ x (I)) \leftrightarrow \exists x \in U k = x (I))$
76	75	elv	$⊢ k \in ran (x \in U ⟼ x (I)) \leftrightarrow \exists x \in U k = x (I)$
77	73 76	sylibr	$⊢ ((((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \land k \in g (I)) \to k \in ran (x \in U ⟼ x (I))$
78	77	ex	$⊢ (((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \to (k \in g (I) \to k \in ran (x \in U ⟼ x (I)))$
79	78	ssrdv	$⊢ (((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \to g (I) \subseteq ran (x \in U ⟼ x (I))$
80		eleq2	$⊢ z = g (I) \to (s (I) \in z \leftrightarrow s (I) \in g (I))$
81		sseq1	$⊢ z = g (I) \to (z \subseteq ran (x \in U ⟼ x (I)) \leftrightarrow g (I) \subseteq ran (x \in U ⟼ x (I)))$
82	80 81	anbi12d	$⊢ z = g (I) \to ((s (I) \in z \land z \subseteq ran (x \in U ⟼ x (I))) \leftrightarrow (s (I) \in g (I) \land g (I) \subseteq ran (x \in U ⟼ x (I))))$
83	82	rspcev	$⊢ (g (I) \in F (I) \land (s (I) \in g (I) \land g (I) \subseteq ran (x \in U ⟼ x (I)))) \to \exists z \in F (I) (s (I) \in z \land z \subseteq ran (x \in U ⟼ x (I)))$
84	31 38 79 83	syl12anc	$⊢ (((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \land (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U)) \to \exists z \in F (I) (s (I) \in z \land z \subseteq ran (x \in U ⟼ x (I)))$
85	84	ex	$⊢ ((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \to ((s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U) \to \exists z \in F (I) (s (I) \in z \land z \subseteq ran (x \in U ⟼ x (I))))$
86		eleq2	$⊢ w = \underset{y \in A}{⨉} g (y) \to (s \in w \leftrightarrow s \in \underset{y \in A}{⨉} g (y))$
87		sseq1	$⊢ w = \underset{y \in A}{⨉} g (y) \to (w \subseteq U \leftrightarrow \underset{y \in A}{⨉} g (y) \subseteq U)$
88	86 87	anbi12d	$⊢ w = \underset{y \in A}{⨉} g (y) \to ((s \in w \land w \subseteq U) \leftrightarrow (s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U))$
89	88	imbi1d	$⊢ w = \underset{y \in A}{⨉} g (y) \to (((s \in w \land w \subseteq U) \to \exists z \in F (I) (s (I) \in z \land z \subseteq ran (x \in U ⟼ x (I)))) \leftrightarrow ((s \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq U) \to \exists z \in F (I) (s (I) \in z \land z \subseteq ran (x \in U ⟼ x (I)))))$
90	85 89	syl5ibrcom	$⊢ ((((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \land (g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y))) \to (w = \underset{y \in A}{⨉} g (y) \to ((s \in w \land w \subseteq U) \to \exists z \in F (I) (s (I) \in z \land z \subseteq ran (x \in U ⟼ x (I)))))$
91	90	expimpd	$⊢ (((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \to (((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land w = \underset{y \in A}{⨉} g (y)) \to ((s \in w \land w \subseteq U) \to \exists z \in F (I) (s (I) \in z \land z \subseteq ran (x \in U ⟼ x (I)))))$
92	91	exlimdv	$⊢ (((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \to (\exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land w = \underset{y \in A}{⨉} g (y)) \to ((s \in w \land w \subseteq U) \to \exists z \in F (I) (s (I) \in z \land z \subseteq ran (x \in U ⟼ x (I)))))$
93	24 92	syl5bi	$⊢ (((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \to (w \in \{s \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land s = \underset{y \in A}{⨉} g (y))\} \to ((s \in w \land w \subseteq U) \to \exists z \in F (I) (s (I) \in z \land z \subseteq ran (x \in U ⟼ x (I)))))$
94	93	rexlimdv	$⊢ (((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \to (\exists w \in \{s \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land s = \underset{y \in A}{⨉} g (y))\} (s \in w \land w \subseteq U) \to \exists z \in F (I) (s (I) \in z \land z \subseteq ran (x \in U ⟼ x (I))))$
95	19 94	mpd	$⊢ (((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \land s \in U) \to \exists z \in F (I) (s (I) \in z \land z \subseteq ran (x \in U ⟼ x (I)))$
96	95	ralrimiva	$⊢ ((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \to \forall s \in U \exists z \in F (I) (s (I) \in z \land z \subseteq ran (x \in U ⟼ x (I)))$
97		fvex	$⊢ s (I) \in V$
98	97	rgenw	$⊢ \forall s \in U s (I) \in V$
99		fveq1	$⊢ x = s \to x (I) = s (I)$
100	99	cbvmptv	$⊢ (x \in U ⟼ x (I)) = (s \in U ⟼ s (I))$
101		eleq1	$⊢ y = s (I) \to (y \in z \leftrightarrow s (I) \in z)$
102	101	anbi1d	$⊢ y = s (I) \to ((y \in z \land z \subseteq ran (x \in U ⟼ x (I))) \leftrightarrow (s (I) \in z \land z \subseteq ran (x \in U ⟼ x (I))))$
103	102	rexbidv	$⊢ y = s (I) \to (\exists z \in F (I) (y \in z \land z \subseteq ran (x \in U ⟼ x (I))) \leftrightarrow \exists z \in F (I) (s (I) \in z \land z \subseteq ran (x \in U ⟼ x (I))))$
104	100 103	ralrnmptw	$⊢ \forall s \in U s (I) \in V \to (\forall y \in ran (x \in U ⟼ x (I)) \exists z \in F (I) (y \in z \land z \subseteq ran (x \in U ⟼ x (I))) \leftrightarrow \forall s \in U \exists z \in F (I) (s (I) \in z \land z \subseteq ran (x \in U ⟼ x (I))))$
105	98 104	ax-mp	$⊢ \forall y \in ran (x \in U ⟼ x (I)) \exists z \in F (I) (y \in z \land z \subseteq ran (x \in U ⟼ x (I))) \leftrightarrow \forall s \in U \exists z \in F (I) (s (I) \in z \land z \subseteq ran (x \in U ⟼ x (I)))$
106	96 105	sylibr	$⊢ ((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \to \forall y \in ran (x \in U ⟼ x (I)) \exists z \in F (I) (y \in z \land z \subseteq ran (x \in U ⟼ x (I)))$
107		simpl2	$⊢ ((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \to F : A ⟶ Top$
108	107 29	ffvelrnd	$⊢ ((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \to F (I) \in Top$
109		eltop2	$⊢ F (I) \in Top \to (ran (x \in U ⟼ x (I)) \in F (I) \leftrightarrow \forall y \in ran (x \in U ⟼ x (I)) \exists z \in F (I) (y \in z \land z \subseteq ran (x \in U ⟼ x (I))))$
110	108 109	syl	$⊢ ((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \to (ran (x \in U ⟼ x (I)) \in F (I) \leftrightarrow \forall y \in ran (x \in U ⟼ x (I)) \exists z \in F (I) (y \in z \land z \subseteq ran (x \in U ⟼ x (I))))$
111	106 110	mpbird	$⊢ ((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \to ran (x \in U ⟼ x (I)) \in F (I)$
112	9 111	eqeltrd	$⊢ ((A \in V \land F : A ⟶ Top \land I \in A) \land U \in J) \to (x \in Y ⟼ x (I)) [U] \in F (I)$

Metamath Proof Explorer

Theorem ptpjopn

Proof