ptcmplem5

	Ref	Expression
Hypotheses	ptcmp.1	$⊢ S = (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
	ptcmp.2	$⊢ X = \underset{n \in A}{⨉} ⋃ F (n)$
	ptcmp.3	$⊢ φ \to A \in V$
	ptcmp.4	$⊢ φ \to F : A ⟶ Comp$
	ptcmp.5	$⊢ φ \to X \in (UFL \cap dom card)$
Assertion	ptcmplem5	$⊢ φ \to \prod_{𝑡} (F) \in Comp$

Proof

Step	Hyp	Ref	Expression
1		ptcmp.1	$⊢ S = (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
2		ptcmp.2	$⊢ X = \underset{n \in A}{⨉} ⋃ F (n)$
3		ptcmp.3	$⊢ φ \to A \in V$
4		ptcmp.4	$⊢ φ \to F : A ⟶ Comp$
5		ptcmp.5	$⊢ φ \to X \in (UFL \cap dom card)$
6	5	elin1d	$⊢ φ \to X \in UFL$
7	1 2 3 4 5	ptcmplem1	$⊢ φ \to (X = ⋃ (ran S \cup \{X\}) \land \prod_{𝑡} (F) = topGen (fi (ran S \cup \{X\})))$
8	7	simpld	$⊢ φ \to X = ⋃ (ran S \cup \{X\})$
9	7	simprd	$⊢ φ \to \prod_{𝑡} (F) = topGen (fi (ran S \cup \{X\}))$
10		elpwi	$⊢ y \in 𝒫 ran S \to y \subseteq ran S$
11	3	ad2antrr	$⊢ ((φ \land (y \subseteq ran S \land X = ⋃ y)) \land \neg \exists z \in (𝒫 y \cap Fin) X = ⋃ z) \to A \in V$
12	4	ad2antrr	$⊢ ((φ \land (y \subseteq ran S \land X = ⋃ y)) \land \neg \exists z \in (𝒫 y \cap Fin) X = ⋃ z) \to F : A ⟶ Comp$
13	5	ad2antrr	$⊢ ((φ \land (y \subseteq ran S \land X = ⋃ y)) \land \neg \exists z \in (𝒫 y \cap Fin) X = ⋃ z) \to X \in (UFL \cap dom card)$
14		simplrl	$⊢ ((φ \land (y \subseteq ran S \land X = ⋃ y)) \land \neg \exists z \in (𝒫 y \cap Fin) X = ⋃ z) \to y \subseteq ran S$
15		simplrr	$⊢ ((φ \land (y \subseteq ran S \land X = ⋃ y)) \land \neg \exists z \in (𝒫 y \cap Fin) X = ⋃ z) \to X = ⋃ y$
16		simpr	$⊢ ((φ \land (y \subseteq ran S \land X = ⋃ y)) \land \neg \exists z \in (𝒫 y \cap Fin) X = ⋃ z) \to \neg \exists z \in (𝒫 y \cap Fin) X = ⋃ z$
17		imaeq2	$⊢ z = u \to {(w \in X ⟼ w (k))}^{-1} [z] = {(w \in X ⟼ w (k))}^{-1} [u]$
18	17	eleq1d	$⊢ z = u \to ({(w \in X ⟼ w (k))}^{-1} [z] \in y \leftrightarrow {(w \in X ⟼ w (k))}^{-1} [u] \in y)$
19	18	cbvrabv	$⊢ \{z \in F (k) \| {(w \in X ⟼ w (k))}^{-1} [z] \in y\} = \{u \in F (k) \| {(w \in X ⟼ w (k))}^{-1} [u] \in y\}$
20	1 2 11 12 13 14 15 16 19	ptcmplem4	$⊢ \neg ((φ \land (y \subseteq ran S \land X = ⋃ y)) \land \neg \exists z \in (𝒫 y \cap Fin) X = ⋃ z)$
21		iman	$⊢ ((φ \land (y \subseteq ran S \land X = ⋃ y)) \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z) \leftrightarrow \neg ((φ \land (y \subseteq ran S \land X = ⋃ y)) \land \neg \exists z \in (𝒫 y \cap Fin) X = ⋃ z)$
22	20 21	mpbir	$⊢ (φ \land (y \subseteq ran S \land X = ⋃ y)) \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z$
23	22	expr	$⊢ (φ \land y \subseteq ran S) \to (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z)$
24	10 23	sylan2	$⊢ (φ \land y \in 𝒫 ran S) \to (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z)$
25	24	adantlr	$⊢ ((φ \land y \subseteq ran S \cup \{X\}) \land y \in 𝒫 ran S) \to (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z)$
26		velpw	$⊢ y \in 𝒫 (ran S \cup \{X\}) \leftrightarrow y \subseteq ran S \cup \{X\}$
27		eldif	$⊢ y \in (𝒫 (ran S \cup \{X\}) ∖ 𝒫 ran S) \leftrightarrow (y \in 𝒫 (ran S \cup \{X\}) \land \neg y \in 𝒫 ran S)$
28		elpwunsn	$⊢ y \in (𝒫 (ran S \cup \{X\}) ∖ 𝒫 ran S) \to X \in y$
29	27 28	sylbir	$⊢ (y \in 𝒫 (ran S \cup \{X\}) \land \neg y \in 𝒫 ran S) \to X \in y$
30	26 29	sylanbr	$⊢ (y \subseteq ran S \cup \{X\} \land \neg y \in 𝒫 ran S) \to X \in y$
31	30	adantll	$⊢ ((φ \land y \subseteq ran S \cup \{X\}) \land \neg y \in 𝒫 ran S) \to X \in y$
32		snssi	$⊢ X \in y \to \{X\} \subseteq y$
33	32	adantl	$⊢ ((φ \land y \subseteq ran S \cup \{X\}) \land X \in y) \to \{X\} \subseteq y$
34		snfi	$⊢ \{X\} \in Fin$
35		elfpw	$⊢ \{X\} \in (𝒫 y \cap Fin) \leftrightarrow (\{X\} \subseteq y \land \{X\} \in Fin)$
36	33 34 35	sylanblrc	$⊢ ((φ \land y \subseteq ran S \cup \{X\}) \land X \in y) \to \{X\} \in (𝒫 y \cap Fin)$
37		unisng	$⊢ X \in y \to ⋃ \{X\} = X$
38	37	eqcomd	$⊢ X \in y \to X = ⋃ \{X\}$
39	38	adantl	$⊢ ((φ \land y \subseteq ran S \cup \{X\}) \land X \in y) \to X = ⋃ \{X\}$
40		unieq	$⊢ z = \{X\} \to ⋃ z = ⋃ \{X\}$
41	40	rspceeqv	$⊢ (\{X\} \in (𝒫 y \cap Fin) \land X = ⋃ \{X\}) \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z$
42	36 39 41	syl2anc	$⊢ ((φ \land y \subseteq ran S \cup \{X\}) \land X \in y) \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z$
43	42	a1d	$⊢ ((φ \land y \subseteq ran S \cup \{X\}) \land X \in y) \to (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z)$
44	31 43	syldan	$⊢ ((φ \land y \subseteq ran S \cup \{X\}) \land \neg y \in 𝒫 ran S) \to (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z)$
45	25 44	pm2.61dan	$⊢ (φ \land y \subseteq ran S \cup \{X\}) \to (X = ⋃ y \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z)$
46	45	impr	$⊢ (φ \land (y \subseteq ran S \cup \{X\} \land X = ⋃ y)) \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z$
47	6 8 9 46	alexsub	$⊢ φ \to \prod_{𝑡} (F) \in Comp$

Metamath Proof Explorer

Theorem ptcmplem5

Proof