ptcmplem3

	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)$
	ptcmplem2.5	$⊢ φ \to U \subseteq ran S$
	ptcmplem2.6	$⊢ φ \to X = ⋃ U$
	ptcmplem2.7	$⊢ φ \to \neg \exists z \in (𝒫 U \cap Fin) X = ⋃ z$
	ptcmplem3.8	$⊢ K = \{u \in F (k) \| {(w \in X ⟼ w (k))}^{-1} [u] \in U\}$
Assertion	ptcmplem3	$⊢ φ \to \exists f (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))$

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		ptcmplem2.5	$⊢ φ \to U \subseteq ran S$
7		ptcmplem2.6	$⊢ φ \to X = ⋃ U$
8		ptcmplem2.7	$⊢ φ \to \neg \exists z \in (𝒫 U \cap Fin) X = ⋃ z$
9		ptcmplem3.8	$⊢ K = \{u \in F (k) \| {(w \in X ⟼ w (k))}^{-1} [u] \in U\}$
10		rabexg	$⊢ A \in V \to \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \in V$
11	3 10	syl	$⊢ φ \to \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \in V$
12	1 2 3 4 5 6 7 8	ptcmplem2	$⊢ φ \to ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} ⋃ F (k) \in dom card$
13		eldifi	$⊢ y \in (⋃ F (k) ∖ ⋃ K) \to y \in ⋃ F (k)$
14	13	3ad2ant3	$⊢ (φ \land y \in V \land y \in (⋃ F (k) ∖ ⋃ K)) \to y \in ⋃ F (k)$
15	14	rabssdv	$⊢ φ \to \{y \in V \| y \in (⋃ F (k) ∖ ⋃ K)\} \subseteq ⋃ F (k)$
16	15	ralrimivw	$⊢ φ \to \forall k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \{y \in V \| y \in (⋃ F (k) ∖ ⋃ K)\} \subseteq ⋃ F (k)$
17		ss2iun	$⊢ \forall k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \{y \in V \| y \in (⋃ F (k) ∖ ⋃ K)\} \subseteq ⋃ F (k) \to ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} \{y \in V \| y \in (⋃ F (k) ∖ ⋃ K)\} \subseteq ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} ⋃ F (k)$
18	16 17	syl	$⊢ φ \to ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} \{y \in V \| y \in (⋃ F (k) ∖ ⋃ K)\} \subseteq ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} ⋃ F (k)$
19		ssnum	$⊢ (⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} ⋃ F (k) \in dom card \land ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} \{y \in V \| y \in (⋃ F (k) ∖ ⋃ K)\} \subseteq ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} ⋃ F (k)) \to ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} \{y \in V \| y \in (⋃ F (k) ∖ ⋃ K)\} \in dom card$
20	12 18 19	syl2anc	$⊢ φ \to ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} \{y \in V \| y \in (⋃ F (k) ∖ ⋃ K)\} \in dom card$
21		elrabi	$⊢ k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \to k \in A$
22	8	adantr	$⊢ (φ \land k \in A) \to \neg \exists z \in (𝒫 U \cap Fin) X = ⋃ z$
23		ssdif0	$⊢ ⋃ F (k) \subseteq ⋃ K \leftrightarrow ⋃ F (k) ∖ ⋃ K = \emptyset$
24	4	ffvelrnda	$⊢ (φ \land k \in A) \to F (k) \in Comp$
25	24	adantr	$⊢ ((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \to F (k) \in Comp$
26	9	ssrab3	$⊢ K \subseteq F (k)$
27	26	a1i	$⊢ ((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \to K \subseteq F (k)$
28		simpr	$⊢ ((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \to ⋃ F (k) \subseteq ⋃ K$
29		uniss	$⊢ K \subseteq F (k) \to ⋃ K \subseteq ⋃ F (k)$
30	26 29	mp1i	$⊢ ((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \to ⋃ K \subseteq ⋃ F (k)$
31	28 30	eqssd	$⊢ ((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \to ⋃ F (k) = ⋃ K$
32		eqid	$⊢ ⋃ F (k) = ⋃ F (k)$
33	32	cmpcov	$⊢ (F (k) \in Comp \land K \subseteq F (k) \land ⋃ F (k) = ⋃ K) \to \exists t \in (𝒫 K \cap Fin) ⋃ F (k) = ⋃ t$
34	25 27 31 33	syl3anc	$⊢ ((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \to \exists t \in (𝒫 K \cap Fin) ⋃ F (k) = ⋃ t$
35		elfpw	$⊢ t \in (𝒫 K \cap Fin) \leftrightarrow (t \subseteq K \land t \in Fin)$
36	35	simplbi	$⊢ t \in (𝒫 K \cap Fin) \to t \subseteq K$
37	36	ad2antrl	$⊢ (((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \to t \subseteq K$
38	37	sselda	$⊢ ((((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \land x \in t) \to x \in K$
39		imaeq2	$⊢ u = x \to {(w \in X ⟼ w (k))}^{-1} [u] = {(w \in X ⟼ w (k))}^{-1} [x]$
40	39	eleq1d	$⊢ u = x \to ({(w \in X ⟼ w (k))}^{-1} [u] \in U \leftrightarrow {(w \in X ⟼ w (k))}^{-1} [x] \in U)$
41	40 9	elrab2	$⊢ x \in K \leftrightarrow (x \in F (k) \land {(w \in X ⟼ w (k))}^{-1} [x] \in U)$
42	41	simprbi	$⊢ x \in K \to {(w \in X ⟼ w (k))}^{-1} [x] \in U$
43	38 42	syl	$⊢ ((((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \land x \in t) \to {(w \in X ⟼ w (k))}^{-1} [x] \in U$
44	43	fmpttd	$⊢ (((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \to (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x]) : t ⟶ U$
45	44	frnd	$⊢ (((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \to ran (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x]) \subseteq U$
46	35	simprbi	$⊢ t \in (𝒫 K \cap Fin) \to t \in Fin$
47	46	ad2antrl	$⊢ (((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \to t \in Fin$
48		eqid	$⊢ (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x]) = (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x])$
49	48	rnmpt	$⊢ ran (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x]) = \{f \| \exists x \in t f = {(w \in X ⟼ w (k))}^{-1} [x]\}$
50		abrexfi	$⊢ t \in Fin \to \{f \| \exists x \in t f = {(w \in X ⟼ w (k))}^{-1} [x]\} \in Fin$
51	49 50	eqeltrid	$⊢ t \in Fin \to ran (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x]) \in Fin$
52	47 51	syl	$⊢ (((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \to ran (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x]) \in Fin$
53		elfpw	$⊢ ran (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x]) \in (𝒫 U \cap Fin) \leftrightarrow (ran (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x]) \subseteq U \land ran (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x]) \in Fin)$
54	45 52 53	sylanbrc	$⊢ (((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \to ran (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x]) \in (𝒫 U \cap Fin)$
55		fveq2	$⊢ n = k \to f (n) = f (k)$
56		fveq2	$⊢ n = k \to F (n) = F (k)$
57	56	unieqd	$⊢ n = k \to ⋃ F (n) = ⋃ F (k)$
58	55 57	eleq12d	$⊢ n = k \to (f (n) \in ⋃ F (n) \leftrightarrow f (k) \in ⋃ F (k))$
59		simpr	$⊢ ((((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \land f \in X) \to f \in X$
60	59 2	eleqtrdi	$⊢ ((((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \land f \in X) \to f \in \underset{n \in A}{⨉} ⋃ F (n)$
61		vex	$⊢ f \in V$
62	61	elixp	$⊢ f \in \underset{n \in A}{⨉} ⋃ F (n) \leftrightarrow (f Fn A \land \forall n \in A f (n) \in ⋃ F (n))$
63	62	simprbi	$⊢ f \in \underset{n \in A}{⨉} ⋃ F (n) \to \forall n \in A f (n) \in ⋃ F (n)$
64	60 63	syl	$⊢ ((((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \land f \in X) \to \forall n \in A f (n) \in ⋃ F (n)$
65		simp-4r	$⊢ ((((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \land f \in X) \to k \in A$
66	58 64 65	rspcdva	$⊢ ((((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \land f \in X) \to f (k) \in ⋃ F (k)$
67		simplrr	$⊢ ((((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \land f \in X) \to ⋃ F (k) = ⋃ t$
68	66 67	eleqtrd	$⊢ ((((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \land f \in X) \to f (k) \in ⋃ t$
69		eluni2	$⊢ f (k) \in ⋃ t \leftrightarrow \exists x \in t f (k) \in x$
70	68 69	sylib	$⊢ ((((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \land f \in X) \to \exists x \in t f (k) \in x$
71		fveq1	$⊢ w = f \to w (k) = f (k)$
72	71	eleq1d	$⊢ w = f \to (w (k) \in x \leftrightarrow f (k) \in x)$
73		eqid	$⊢ (w \in X ⟼ w (k)) = (w \in X ⟼ w (k))$
74	73	mptpreima	$⊢ {(w \in X ⟼ w (k))}^{-1} [x] = \{w \in X \| w (k) \in x\}$
75	72 74	elrab2	$⊢ f \in {(w \in X ⟼ w (k))}^{-1} [x] \leftrightarrow (f \in X \land f (k) \in x)$
76	75	baib	$⊢ f \in X \to (f \in {(w \in X ⟼ w (k))}^{-1} [x] \leftrightarrow f (k) \in x)$
77	76	ad2antlr	$⊢ (((((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \land f \in X) \land x \in t) \to (f \in {(w \in X ⟼ w (k))}^{-1} [x] \leftrightarrow f (k) \in x)$
78	77	rexbidva	$⊢ ((((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \land f \in X) \to (\exists x \in t f \in {(w \in X ⟼ w (k))}^{-1} [x] \leftrightarrow \exists x \in t f (k) \in x)$
79	70 78	mpbird	$⊢ ((((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \land f \in X) \to \exists x \in t f \in {(w \in X ⟼ w (k))}^{-1} [x]$
80		eliun	$⊢ f \in ⋃_{x \in t} {(w \in X ⟼ w (k))}^{-1} [x] \leftrightarrow \exists x \in t f \in {(w \in X ⟼ w (k))}^{-1} [x]$
81	79 80	sylibr	$⊢ ((((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \land f \in X) \to f \in ⋃_{x \in t} {(w \in X ⟼ w (k))}^{-1} [x]$
82	81	ex	$⊢ (((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \to (f \in X \to f \in ⋃_{x \in t} {(w \in X ⟼ w (k))}^{-1} [x])$
83	82	ssrdv	$⊢ (((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \to X \subseteq ⋃_{x \in t} {(w \in X ⟼ w (k))}^{-1} [x]$
84	43	ralrimiva	$⊢ (((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \to \forall x \in t {(w \in X ⟼ w (k))}^{-1} [x] \in U$
85		dfiun2g	$⊢ \forall x \in t {(w \in X ⟼ w (k))}^{-1} [x] \in U \to ⋃_{x \in t} {(w \in X ⟼ w (k))}^{-1} [x] = ⋃ \{f \| \exists x \in t f = {(w \in X ⟼ w (k))}^{-1} [x]\}$
86	84 85	syl	$⊢ (((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \to ⋃_{x \in t} {(w \in X ⟼ w (k))}^{-1} [x] = ⋃ \{f \| \exists x \in t f = {(w \in X ⟼ w (k))}^{-1} [x]\}$
87	49	unieqi	$⊢ ⋃ ran (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x]) = ⋃ \{f \| \exists x \in t f = {(w \in X ⟼ w (k))}^{-1} [x]\}$
88	86 87	eqtr4di	$⊢ (((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \to ⋃_{x \in t} {(w \in X ⟼ w (k))}^{-1} [x] = ⋃ ran (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x])$
89	83 88	sseqtrd	$⊢ (((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \to X \subseteq ⋃ ran (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x])$
90	45	unissd	$⊢ (((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \to ⋃ ran (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x]) \subseteq ⋃ U$
91	7	ad3antrrr	$⊢ (((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \to X = ⋃ U$
92	90 91	sseqtrrd	$⊢ (((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \to ⋃ ran (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x]) \subseteq X$
93	89 92	eqssd	$⊢ (((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \to X = ⋃ ran (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x])$
94		unieq	$⊢ z = ran (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x]) \to ⋃ z = ⋃ ran (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x])$
95	94	rspceeqv	$⊢ (ran (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x]) \in (𝒫 U \cap Fin) \land X = ⋃ ran (x \in t ⟼ {(w \in X ⟼ w (k))}^{-1} [x])) \to \exists z \in (𝒫 U \cap Fin) X = ⋃ z$
96	54 93 95	syl2anc	$⊢ (((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \land (t \in (𝒫 K \cap Fin) \land ⋃ F (k) = ⋃ t)) \to \exists z \in (𝒫 U \cap Fin) X = ⋃ z$
97	34 96	rexlimddv	$⊢ ((φ \land k \in A) \land ⋃ F (k) \subseteq ⋃ K) \to \exists z \in (𝒫 U \cap Fin) X = ⋃ z$
98	97	ex	$⊢ (φ \land k \in A) \to (⋃ F (k) \subseteq ⋃ K \to \exists z \in (𝒫 U \cap Fin) X = ⋃ z)$
99	23 98	syl5bir	$⊢ (φ \land k \in A) \to (⋃ F (k) ∖ ⋃ K = \emptyset \to \exists z \in (𝒫 U \cap Fin) X = ⋃ z)$
100	22 99	mtod	$⊢ (φ \land k \in A) \to \neg ⋃ F (k) ∖ ⋃ K = \emptyset$
101		neq0	$⊢ \neg ⋃ F (k) ∖ ⋃ K = \emptyset \leftrightarrow \exists y y \in (⋃ F (k) ∖ ⋃ K)$
102	100 101	sylib	$⊢ (φ \land k \in A) \to \exists y y \in (⋃ F (k) ∖ ⋃ K)$
103		rexv	$⊢ \exists y \in V y \in (⋃ F (k) ∖ ⋃ K) \leftrightarrow \exists y y \in (⋃ F (k) ∖ ⋃ K)$
104	102 103	sylibr	$⊢ (φ \land k \in A) \to \exists y \in V y \in (⋃ F (k) ∖ ⋃ K)$
105	21 104	sylan2	$⊢ (φ \land k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}) \to \exists y \in V y \in (⋃ F (k) ∖ ⋃ K)$
106	105	ralrimiva	$⊢ φ \to \forall k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \exists y \in V y \in (⋃ F (k) ∖ ⋃ K)$
107		eleq1	$⊢ y = g (k) \to (y \in (⋃ F (k) ∖ ⋃ K) \leftrightarrow g (k) \in (⋃ F (k) ∖ ⋃ K))$
108	107	ac6num	$⊢ (\{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \in V \land ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} \{y \in V \| y \in (⋃ F (k) ∖ ⋃ K)\} \in dom card \land \forall k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \exists y \in V y \in (⋃ F (k) ∖ ⋃ K)) \to \exists g (g : \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} ⟶ V \land \forall k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} g (k) \in (⋃ F (k) ∖ ⋃ K))$
109	11 20 106 108	syl3anc	$⊢ φ \to \exists g (g : \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} ⟶ V \land \forall k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} g (k) \in (⋃ F (k) ∖ ⋃ K))$
110	3	adantr	$⊢ (φ \land (g : \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} ⟶ V \land \forall k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} g (k) \in (⋃ F (k) ∖ ⋃ K))) \to A \in V$
111	110	mptexd	$⊢ (φ \land (g : \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} ⟶ V \land \forall k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} g (k) \in (⋃ F (k) ∖ ⋃ K))) \to (m \in A ⟼ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m))) \in V$
112		fvex	$⊢ F (m) \in V$
113	112	uniex	$⊢ ⋃ F (m) \in V$
114	113	uniex	$⊢ ⋃ ⋃ F (m) \in V$
115		fvex	$⊢ g (m) \in V$
116	114 115	ifex	$⊢ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m)) \in V$
117	116	rgenw	$⊢ \forall m \in A if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m)) \in V$
118		eqid	$⊢ (m \in A ⟼ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m))) = (m \in A ⟼ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m)))$
119	118	fnmpt	$⊢ \forall m \in A if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m)) \in V \to (m \in A ⟼ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m))) Fn A$
120	117 119	mp1i	$⊢ (φ \land (g : \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} ⟶ V \land \forall k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} g (k) \in (⋃ F (k) ∖ ⋃ K))) \to (m \in A ⟼ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m))) Fn A$
121	57	breq1d	$⊢ n = k \to (⋃ F (n) \approx 1_{𝑜} \leftrightarrow ⋃ F (k) \approx 1_{𝑜})$
122	121	notbid	$⊢ n = k \to (\neg ⋃ F (n) \approx 1_{𝑜} \leftrightarrow \neg ⋃ F (k) \approx 1_{𝑜})$
123	122	ralrab	$⊢ \forall k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} g (k) \in (⋃ F (k) ∖ ⋃ K) \leftrightarrow \forall k \in A (\neg ⋃ F (k) \approx 1_{𝑜} \to g (k) \in (⋃ F (k) ∖ ⋃ K))$
124		iftrue	$⊢ ⋃ F (k) \approx 1_{𝑜} \to if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k)) = ⋃ ⋃ F (k)$
125	124	ad2antll	$⊢ ((φ \land g : \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} ⟶ V) \land (k \in A \land ⋃ F (k) \approx 1_{𝑜})) \to if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k)) = ⋃ ⋃ F (k)$
126	102	adantrr	$⊢ (φ \land (k \in A \land ⋃ F (k) \approx 1_{𝑜})) \to \exists y y \in (⋃ F (k) ∖ ⋃ K)$
127	13	adantl	$⊢ ((φ \land (k \in A \land ⋃ F (k) \approx 1_{𝑜})) \land y \in (⋃ F (k) ∖ ⋃ K)) \to y \in ⋃ F (k)$
128		simplrr	$⊢ ((φ \land (k \in A \land ⋃ F (k) \approx 1_{𝑜})) \land y \in (⋃ F (k) ∖ ⋃ K)) \to ⋃ F (k) \approx 1_{𝑜}$
129		en1b	$⊢ ⋃ F (k) \approx 1_{𝑜} \leftrightarrow ⋃ F (k) = \{⋃ ⋃ F (k)\}$
130	128 129	sylib	$⊢ ((φ \land (k \in A \land ⋃ F (k) \approx 1_{𝑜})) \land y \in (⋃ F (k) ∖ ⋃ K)) \to ⋃ F (k) = \{⋃ ⋃ F (k)\}$
131	127 130	eleqtrd	$⊢ ((φ \land (k \in A \land ⋃ F (k) \approx 1_{𝑜})) \land y \in (⋃ F (k) ∖ ⋃ K)) \to y \in \{⋃ ⋃ F (k)\}$
132		elsni	$⊢ y \in \{⋃ ⋃ F (k)\} \to y = ⋃ ⋃ F (k)$
133	131 132	syl	$⊢ ((φ \land (k \in A \land ⋃ F (k) \approx 1_{𝑜})) \land y \in (⋃ F (k) ∖ ⋃ K)) \to y = ⋃ ⋃ F (k)$
134		simpr	$⊢ ((φ \land (k \in A \land ⋃ F (k) \approx 1_{𝑜})) \land y \in (⋃ F (k) ∖ ⋃ K)) \to y \in (⋃ F (k) ∖ ⋃ K)$
135	133 134	eqeltrrd	$⊢ ((φ \land (k \in A \land ⋃ F (k) \approx 1_{𝑜})) \land y \in (⋃ F (k) ∖ ⋃ K)) \to ⋃ ⋃ F (k) \in (⋃ F (k) ∖ ⋃ K)$
136	126 135	exlimddv	$⊢ (φ \land (k \in A \land ⋃ F (k) \approx 1_{𝑜})) \to ⋃ ⋃ F (k) \in (⋃ F (k) ∖ ⋃ K)$
137	136	adantlr	$⊢ ((φ \land g : \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} ⟶ V) \land (k \in A \land ⋃ F (k) \approx 1_{𝑜})) \to ⋃ ⋃ F (k) \in (⋃ F (k) ∖ ⋃ K)$
138	125 137	eqeltrd	$⊢ ((φ \land g : \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} ⟶ V) \land (k \in A \land ⋃ F (k) \approx 1_{𝑜})) \to if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k)) \in (⋃ F (k) ∖ ⋃ K)$
139	138	a1d	$⊢ ((φ \land g : \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} ⟶ V) \land (k \in A \land ⋃ F (k) \approx 1_{𝑜})) \to ((\neg ⋃ F (k) \approx 1_{𝑜} \to g (k) \in (⋃ F (k) ∖ ⋃ K)) \to if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k)) \in (⋃ F (k) ∖ ⋃ K))$
140	139	expr	$⊢ ((φ \land g : \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} ⟶ V) \land k \in A) \to (⋃ F (k) \approx 1_{𝑜} \to ((\neg ⋃ F (k) \approx 1_{𝑜} \to g (k) \in (⋃ F (k) ∖ ⋃ K)) \to if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k)) \in (⋃ F (k) ∖ ⋃ K)))$
141		pm2.27	$⊢ \neg ⋃ F (k) \approx 1_{𝑜} \to ((\neg ⋃ F (k) \approx 1_{𝑜} \to g (k) \in (⋃ F (k) ∖ ⋃ K)) \to g (k) \in (⋃ F (k) ∖ ⋃ K))$
142		iffalse	$⊢ \neg ⋃ F (k) \approx 1_{𝑜} \to if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k)) = g (k)$
143	142	eleq1d	$⊢ \neg ⋃ F (k) \approx 1_{𝑜} \to (if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k)) \in (⋃ F (k) ∖ ⋃ K) \leftrightarrow g (k) \in (⋃ F (k) ∖ ⋃ K))$
144	141 143	sylibrd	$⊢ \neg ⋃ F (k) \approx 1_{𝑜} \to ((\neg ⋃ F (k) \approx 1_{𝑜} \to g (k) \in (⋃ F (k) ∖ ⋃ K)) \to if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k)) \in (⋃ F (k) ∖ ⋃ K))$
145	140 144	pm2.61d1	$⊢ ((φ \land g : \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} ⟶ V) \land k \in A) \to ((\neg ⋃ F (k) \approx 1_{𝑜} \to g (k) \in (⋃ F (k) ∖ ⋃ K)) \to if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k)) \in (⋃ F (k) ∖ ⋃ K))$
146	145	ralimdva	$⊢ (φ \land g : \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} ⟶ V) \to (\forall k \in A (\neg ⋃ F (k) \approx 1_{𝑜} \to g (k) \in (⋃ F (k) ∖ ⋃ K)) \to \forall k \in A if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k)) \in (⋃ F (k) ∖ ⋃ K))$
147	123 146	syl5bi	$⊢ (φ \land g : \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} ⟶ V) \to (\forall k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} g (k) \in (⋃ F (k) ∖ ⋃ K) \to \forall k \in A if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k)) \in (⋃ F (k) ∖ ⋃ K))$
148	147	impr	$⊢ (φ \land (g : \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} ⟶ V \land \forall k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} g (k) \in (⋃ F (k) ∖ ⋃ K))) \to \forall k \in A if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k)) \in (⋃ F (k) ∖ ⋃ K)$
149		fneq1	$⊢ f = (m \in A ⟼ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m))) \to (f Fn A \leftrightarrow (m \in A ⟼ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m))) Fn A)$
150		fveq1	$⊢ f = (m \in A ⟼ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m))) \to f (k) = (m \in A ⟼ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m))) (k)$
151		fveq2	$⊢ m = k \to F (m) = F (k)$
152	151	unieqd	$⊢ m = k \to ⋃ F (m) = ⋃ F (k)$
153	152	breq1d	$⊢ m = k \to (⋃ F (m) \approx 1_{𝑜} \leftrightarrow ⋃ F (k) \approx 1_{𝑜})$
154	152	unieqd	$⊢ m = k \to ⋃ ⋃ F (m) = ⋃ ⋃ F (k)$
155		fveq2	$⊢ m = k \to g (m) = g (k)$
156	153 154 155	ifbieq12d	$⊢ m = k \to if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m)) = if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k))$
157		fvex	$⊢ F (k) \in V$
158	157	uniex	$⊢ ⋃ F (k) \in V$
159	158	uniex	$⊢ ⋃ ⋃ F (k) \in V$
160		fvex	$⊢ g (k) \in V$
161	159 160	ifex	$⊢ if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k)) \in V$
162	156 118 161	fvmpt	$⊢ k \in A \to (m \in A ⟼ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m))) (k) = if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k))$
163	150 162	sylan9eq	$⊢ (f = (m \in A ⟼ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m))) \land k \in A) \to f (k) = if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k))$
164	163	eleq1d	$⊢ (f = (m \in A ⟼ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m))) \land k \in A) \to (f (k) \in (⋃ F (k) ∖ ⋃ K) \leftrightarrow if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k)) \in (⋃ F (k) ∖ ⋃ K))$
165	164	ralbidva	$⊢ f = (m \in A ⟼ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m))) \to (\forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K) \leftrightarrow \forall k \in A if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k)) \in (⋃ F (k) ∖ ⋃ K))$
166	149 165	anbi12d	$⊢ f = (m \in A ⟼ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m))) \to ((f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K)) \leftrightarrow ((m \in A ⟼ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m))) Fn A \land \forall k \in A if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k)) \in (⋃ F (k) ∖ ⋃ K)))$
167	166	spcegv	$⊢ (m \in A ⟼ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m))) \in V \to (((m \in A ⟼ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m))) Fn A \land \forall k \in A if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k)) \in (⋃ F (k) ∖ ⋃ K)) \to \exists f (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K)))$
168	167	3impib	$⊢ ((m \in A ⟼ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m))) \in V \land (m \in A ⟼ if (⋃ F (m) \approx 1_{𝑜}, ⋃ ⋃ F (m), g (m))) Fn A \land \forall k \in A if (⋃ F (k) \approx 1_{𝑜}, ⋃ ⋃ F (k), g (k)) \in (⋃ F (k) ∖ ⋃ K)) \to \exists f (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))$
169	111 120 148 168	syl3anc	$⊢ (φ \land (g : \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} ⟶ V \land \forall k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} g (k) \in (⋃ F (k) ∖ ⋃ K))) \to \exists f (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))$
170	109 169	exlimddv	$⊢ φ \to \exists f (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))$

Metamath Proof Explorer

Theorem ptcmplem3

Proof