ptcmplem2

	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$
Assertion	ptcmplem2	$⊢ φ \to ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} ⋃ F (k) \in dom card$

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		0ss	$⊢ \emptyset \subseteq U$
10		0fin	$⊢ \emptyset \in Fin$
11		elfpw	$⊢ \emptyset \in (𝒫 U \cap Fin) \leftrightarrow (\emptyset \subseteq U \land \emptyset \in Fin)$
12	9 10 11	mpbir2an	$⊢ \emptyset \in (𝒫 U \cap Fin)$
13		unieq	$⊢ z = \emptyset \to ⋃ z = ⋃ \emptyset$
14		uni0	$⊢ ⋃ \emptyset = \emptyset$
15	13 14	syl6eq	$⊢ z = \emptyset \to ⋃ z = \emptyset$
16	15	rspceeqv	$⊢ (\emptyset \in (𝒫 U \cap Fin) \land X = \emptyset) \to \exists z \in (𝒫 U \cap Fin) X = ⋃ z$
17	12 16	mpan	$⊢ X = \emptyset \to \exists z \in (𝒫 U \cap Fin) X = ⋃ z$
18	17	necon3bi	$⊢ \neg \exists z \in (𝒫 U \cap Fin) X = ⋃ z \to X \neq \emptyset$
19	8 18	syl	$⊢ φ \to X \neq \emptyset$
20		n0	$⊢ X \neq \emptyset \leftrightarrow \exists f f \in X$
21	19 20	sylib	$⊢ φ \to \exists f f \in X$
22		fveq2	$⊢ n = k \to F (n) = F (k)$
23	22	unieqd	$⊢ n = k \to ⋃ F (n) = ⋃ F (k)$
24	23	cbvixpv	$⊢ \underset{n \in A}{⨉} ⋃ F (n) = \underset{k \in A}{⨉} ⋃ F (k)$
25	2 24	eqtri	$⊢ X = \underset{k \in A}{⨉} ⋃ F (k)$
26	5	elin2d	$⊢ φ \to X \in dom card$
27	26	adantr	$⊢ (φ \land f \in X) \to X \in dom card$
28	25 27	eqeltrrid	$⊢ (φ \land f \in X) \to \underset{k \in A}{⨉} ⋃ F (k) \in dom card$
29		ssrab2	$⊢ \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \subseteq A$
30	19	adantr	$⊢ (φ \land f \in X) \to X \neq \emptyset$
31	25 30	eqnetrrid	$⊢ (φ \land f \in X) \to \underset{k \in A}{⨉} ⋃ F (k) \neq \emptyset$
32		eqid	$⊢ (g \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ {g ↾}_{\{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}) = (g \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ {g ↾}_{\{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}})$
33	32	resixpfo	$⊢ (\{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \subseteq A \land \underset{k \in A}{⨉} ⋃ F (k) \neq \emptyset) \to (g \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ {g ↾}_{\{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}) : \underset{k \in A}{⨉} ⋃ F (k) \underset{onto}{⟶} \underset{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}{⨉} ⋃ F (k)$
34	29 31 33	sylancr	$⊢ (φ \land f \in X) \to (g \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ {g ↾}_{\{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}) : \underset{k \in A}{⨉} ⋃ F (k) \underset{onto}{⟶} \underset{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}{⨉} ⋃ F (k)$
35		fonum	$⊢ (\underset{k \in A}{⨉} ⋃ F (k) \in dom card \land (g \in \underset{k \in A}{⨉} ⋃ F (k) ⟼ {g ↾}_{\{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}) : \underset{k \in A}{⨉} ⋃ F (k) \underset{onto}{⟶} \underset{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}{⨉} ⋃ F (k)) \to \underset{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}{⨉} ⋃ F (k) \in dom card$
36	28 34 35	syl2anc	$⊢ (φ \land f \in X) \to \underset{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}{⨉} ⋃ F (k) \in dom card$
37		vex	$⊢ g \in V$
38		difexg	$⊢ g \in V \to g ∖ f \in V$
39	37 38	mp1i	$⊢ (φ \land f \in X) \to g ∖ f \in V$
40		dmexg	$⊢ g ∖ f \in V \to dom (g ∖ f) \in V$
41		uniexg	$⊢ dom (g ∖ f) \in V \to ⋃ dom (g ∖ f) \in V$
42	39 40 41	3syl	$⊢ (φ \land f \in X) \to ⋃ dom (g ∖ f) \in V$
43	42	ralrimivw	$⊢ (φ \land f \in X) \to \forall g \in X ⋃ dom (g ∖ f) \in V$
44		eqid	$⊢ (g \in X ⟼ ⋃ dom (g ∖ f)) = (g \in X ⟼ ⋃ dom (g ∖ f))$
45	44	fnmpt	$⊢ \forall g \in X ⋃ dom (g ∖ f) \in V \to (g \in X ⟼ ⋃ dom (g ∖ f)) Fn X$
46	43 45	syl	$⊢ (φ \land f \in X) \to (g \in X ⟼ ⋃ dom (g ∖ f)) Fn X$
47		dffn4	$⊢ (g \in X ⟼ ⋃ dom (g ∖ f)) Fn X \leftrightarrow (g \in X ⟼ ⋃ dom (g ∖ f)) : X \underset{onto}{⟶} ran (g \in X ⟼ ⋃ dom (g ∖ f))$
48	46 47	sylib	$⊢ (φ \land f \in X) \to (g \in X ⟼ ⋃ dom (g ∖ f)) : X \underset{onto}{⟶} ran (g \in X ⟼ ⋃ dom (g ∖ f))$
49		fonum	$⊢ (X \in dom card \land (g \in X ⟼ ⋃ dom (g ∖ f)) : X \underset{onto}{⟶} ran (g \in X ⟼ ⋃ dom (g ∖ f))) \to ran (g \in X ⟼ ⋃ dom (g ∖ f)) \in dom card$
50	27 48 49	syl2anc	$⊢ (φ \land f \in X) \to ran (g \in X ⟼ ⋃ dom (g ∖ f)) \in dom card$
51		ssdif0	$⊢ ⋃ F (k) \subseteq \{f (k)\} \leftrightarrow ⋃ F (k) ∖ \{f (k)\} = \emptyset$
52		simpr	$⊢ (((φ \land f \in X) \land k \in A) \land ⋃ F (k) \subseteq \{f (k)\}) \to ⋃ F (k) \subseteq \{f (k)\}$
53		simpr	$⊢ (φ \land f \in X) \to f \in X$
54	53 25	eleqtrdi	$⊢ (φ \land f \in X) \to f \in \underset{k \in A}{⨉} ⋃ F (k)$
55		vex	$⊢ f \in V$
56	55	elixp	$⊢ f \in \underset{k \in A}{⨉} ⋃ F (k) \leftrightarrow (f Fn A \land \forall k \in A f (k) \in ⋃ F (k))$
57	56	simprbi	$⊢ f \in \underset{k \in A}{⨉} ⋃ F (k) \to \forall k \in A f (k) \in ⋃ F (k)$
58	54 57	syl	$⊢ (φ \land f \in X) \to \forall k \in A f (k) \in ⋃ F (k)$
59	58	r19.21bi	$⊢ ((φ \land f \in X) \land k \in A) \to f (k) \in ⋃ F (k)$
60	59	snssd	$⊢ ((φ \land f \in X) \land k \in A) \to \{f (k)\} \subseteq ⋃ F (k)$
61	60	adantr	$⊢ (((φ \land f \in X) \land k \in A) \land ⋃ F (k) \subseteq \{f (k)\}) \to \{f (k)\} \subseteq ⋃ F (k)$
62	52 61	eqssd	$⊢ (((φ \land f \in X) \land k \in A) \land ⋃ F (k) \subseteq \{f (k)\}) \to ⋃ F (k) = \{f (k)\}$
63		fvex	$⊢ f (k) \in V$
64	63	ensn1	$⊢ \{f (k)\} \approx 1_{𝑜}$
65	62 64	eqbrtrdi	$⊢ (((φ \land f \in X) \land k \in A) \land ⋃ F (k) \subseteq \{f (k)\}) \to ⋃ F (k) \approx 1_{𝑜}$
66	65	ex	$⊢ ((φ \land f \in X) \land k \in A) \to (⋃ F (k) \subseteq \{f (k)\} \to ⋃ F (k) \approx 1_{𝑜})$
67	51 66	syl5bir	$⊢ ((φ \land f \in X) \land k \in A) \to (⋃ F (k) ∖ \{f (k)\} = \emptyset \to ⋃ F (k) \approx 1_{𝑜})$
68	67	con3d	$⊢ ((φ \land f \in X) \land k \in A) \to (\neg ⋃ F (k) \approx 1_{𝑜} \to \neg ⋃ F (k) ∖ \{f (k)\} = \emptyset)$
69		neq0	$⊢ \neg ⋃ F (k) ∖ \{f (k)\} = \emptyset \leftrightarrow \exists x x \in (⋃ F (k) ∖ \{f (k)\})$
70	68 69	syl6ib	$⊢ ((φ \land f \in X) \land k \in A) \to (\neg ⋃ F (k) \approx 1_{𝑜} \to \exists x x \in (⋃ F (k) ∖ \{f (k)\}))$
71		eldifi	$⊢ x \in (⋃ F (k) ∖ \{f (k)\}) \to x \in ⋃ F (k)$
72		simplr	$⊢ ((((φ \land f \in X) \land k \in A) \land x \in ⋃ F (k)) \land n \in A) \to x \in ⋃ F (k)$
73		iftrue	$⊢ n = k \to if (n = k, x, f (n)) = x$
74	73 23	eleq12d	$⊢ n = k \to (if (n = k, x, f (n)) \in ⋃ F (n) \leftrightarrow x \in ⋃ F (k))$
75	72 74	syl5ibrcom	$⊢ ((((φ \land f \in X) \land k \in A) \land x \in ⋃ F (k)) \land n \in A) \to (n = k \to if (n = k, x, f (n)) \in ⋃ F (n))$
76	53 2	eleqtrdi	$⊢ (φ \land f \in X) \to f \in \underset{n \in A}{⨉} ⋃ F (n)$
77	55	elixp	$⊢ f \in \underset{n \in A}{⨉} ⋃ F (n) \leftrightarrow (f Fn A \land \forall n \in A f (n) \in ⋃ F (n))$
78	77	simprbi	$⊢ f \in \underset{n \in A}{⨉} ⋃ F (n) \to \forall n \in A f (n) \in ⋃ F (n)$
79	76 78	syl	$⊢ (φ \land f \in X) \to \forall n \in A f (n) \in ⋃ F (n)$
80	79	ad2antrr	$⊢ (((φ \land f \in X) \land k \in A) \land x \in ⋃ F (k)) \to \forall n \in A f (n) \in ⋃ F (n)$
81	80	r19.21bi	$⊢ ((((φ \land f \in X) \land k \in A) \land x \in ⋃ F (k)) \land n \in A) \to f (n) \in ⋃ F (n)$
82		iffalse	$⊢ \neg n = k \to if (n = k, x, f (n)) = f (n)$
83	82	eleq1d	$⊢ \neg n = k \to (if (n = k, x, f (n)) \in ⋃ F (n) \leftrightarrow f (n) \in ⋃ F (n))$
84	81 83	syl5ibrcom	$⊢ ((((φ \land f \in X) \land k \in A) \land x \in ⋃ F (k)) \land n \in A) \to (\neg n = k \to if (n = k, x, f (n)) \in ⋃ F (n))$
85	75 84	pm2.61d	$⊢ ((((φ \land f \in X) \land k \in A) \land x \in ⋃ F (k)) \land n \in A) \to if (n = k, x, f (n)) \in ⋃ F (n)$
86	85	ralrimiva	$⊢ (((φ \land f \in X) \land k \in A) \land x \in ⋃ F (k)) \to \forall n \in A if (n = k, x, f (n)) \in ⋃ F (n)$
87	3	ad3antrrr	$⊢ (((φ \land f \in X) \land k \in A) \land x \in ⋃ F (k)) \to A \in V$
88		mptelixpg	$⊢ A \in V \to ((n \in A ⟼ if (n = k, x, f (n))) \in \underset{n \in A}{⨉} ⋃ F (n) \leftrightarrow \forall n \in A if (n = k, x, f (n)) \in ⋃ F (n))$
89	87 88	syl	$⊢ (((φ \land f \in X) \land k \in A) \land x \in ⋃ F (k)) \to ((n \in A ⟼ if (n = k, x, f (n))) \in \underset{n \in A}{⨉} ⋃ F (n) \leftrightarrow \forall n \in A if (n = k, x, f (n)) \in ⋃ F (n))$
90	86 89	mpbird	$⊢ (((φ \land f \in X) \land k \in A) \land x \in ⋃ F (k)) \to (n \in A ⟼ if (n = k, x, f (n))) \in \underset{n \in A}{⨉} ⋃ F (n)$
91	90 2	eleqtrrdi	$⊢ (((φ \land f \in X) \land k \in A) \land x \in ⋃ F (k)) \to (n \in A ⟼ if (n = k, x, f (n))) \in X$
92	71 91	sylan2	$⊢ (((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \to (n \in A ⟼ if (n = k, x, f (n))) \in X$
93		vex	$⊢ k \in V$
94	93	unisn	$⊢ ⋃ \{k\} = k$
95		simplr	$⊢ (((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \to k \in A$
96		eleq1w	$⊢ m = k \to (m \in A \leftrightarrow k \in A)$
97	95 96	syl5ibrcom	$⊢ (((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \to (m = k \to m \in A)$
98	97	pm4.71rd	$⊢ (((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \to (m = k \leftrightarrow (m \in A \land m = k))$
99		equequ1	$⊢ n = m \to (n = k \leftrightarrow m = k)$
100		fveq2	$⊢ n = m \to f (n) = f (m)$
101	99 100	ifbieq2d	$⊢ n = m \to if (n = k, x, f (n)) = if (m = k, x, f (m))$
102		eqid	$⊢ (n \in A ⟼ if (n = k, x, f (n))) = (n \in A ⟼ if (n = k, x, f (n)))$
103		vex	$⊢ x \in V$
104		fvex	$⊢ f (m) \in V$
105	103 104	ifex	$⊢ if (m = k, x, f (m)) \in V$
106	101 102 105	fvmpt	$⊢ m \in A \to (n \in A ⟼ if (n = k, x, f (n))) (m) = if (m = k, x, f (m))$
107	106	neeq1d	$⊢ m \in A \to ((n \in A ⟼ if (n = k, x, f (n))) (m) \neq f (m) \leftrightarrow if (m = k, x, f (m)) \neq f (m))$
108	107	adantl	$⊢ ((((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \land m \in A) \to ((n \in A ⟼ if (n = k, x, f (n))) (m) \neq f (m) \leftrightarrow if (m = k, x, f (m)) \neq f (m))$
109		iffalse	$⊢ \neg m = k \to if (m = k, x, f (m)) = f (m)$
110	109	necon1ai	$⊢ if (m = k, x, f (m)) \neq f (m) \to m = k$
111		eldifsni	$⊢ x \in (⋃ F (k) ∖ \{f (k)\}) \to x \neq f (k)$
112	111	ad2antlr	$⊢ ((((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \land m \in A) \to x \neq f (k)$
113		iftrue	$⊢ m = k \to if (m = k, x, f (m)) = x$
114		fveq2	$⊢ m = k \to f (m) = f (k)$
115	113 114	neeq12d	$⊢ m = k \to (if (m = k, x, f (m)) \neq f (m) \leftrightarrow x \neq f (k))$
116	112 115	syl5ibrcom	$⊢ ((((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \land m \in A) \to (m = k \to if (m = k, x, f (m)) \neq f (m))$
117	110 116	impbid2	$⊢ ((((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \land m \in A) \to (if (m = k, x, f (m)) \neq f (m) \leftrightarrow m = k)$
118	108 117	bitrd	$⊢ ((((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \land m \in A) \to ((n \in A ⟼ if (n = k, x, f (n))) (m) \neq f (m) \leftrightarrow m = k)$
119	118	pm5.32da	$⊢ (((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \to ((m \in A \land (n \in A ⟼ if (n = k, x, f (n))) (m) \neq f (m)) \leftrightarrow (m \in A \land m = k))$
120	98 119	bitr4d	$⊢ (((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \to (m = k \leftrightarrow (m \in A \land (n \in A ⟼ if (n = k, x, f (n))) (m) \neq f (m)))$
121	120	abbidv	$⊢ (((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \to \{m \| m = k\} = \{m \| (m \in A \land (n \in A ⟼ if (n = k, x, f (n))) (m) \neq f (m))\}$
122		df-sn	$⊢ \{k\} = \{m \| m = k\}$
123		df-rab	$⊢ \{m \in A \| (n \in A ⟼ if (n = k, x, f (n))) (m) \neq f (m)\} = \{m \| (m \in A \land (n \in A ⟼ if (n = k, x, f (n))) (m) \neq f (m))\}$
124	121 122 123	3eqtr4g	$⊢ (((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \to \{k\} = \{m \in A \| (n \in A ⟼ if (n = k, x, f (n))) (m) \neq f (m)\}$
125		fvex	$⊢ f (n) \in V$
126	103 125	ifex	$⊢ if (n = k, x, f (n)) \in V$
127	126	rgenw	$⊢ \forall n \in A if (n = k, x, f (n)) \in V$
128	102	fnmpt	$⊢ \forall n \in A if (n = k, x, f (n)) \in V \to (n \in A ⟼ if (n = k, x, f (n))) Fn A$
129	127 128	mp1i	$⊢ (((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \to (n \in A ⟼ if (n = k, x, f (n))) Fn A$
130		ixpfn	$⊢ f \in \underset{n \in A}{⨉} ⋃ F (n) \to f Fn A$
131	76 130	syl	$⊢ (φ \land f \in X) \to f Fn A$
132	131	ad2antrr	$⊢ (((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \to f Fn A$
133		fndmdif	$⊢ ((n \in A ⟼ if (n = k, x, f (n))) Fn A \land f Fn A) \to dom ((n \in A ⟼ if (n = k, x, f (n))) ∖ f) = \{m \in A \| (n \in A ⟼ if (n = k, x, f (n))) (m) \neq f (m)\}$
134	129 132 133	syl2anc	$⊢ (((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \to dom ((n \in A ⟼ if (n = k, x, f (n))) ∖ f) = \{m \in A \| (n \in A ⟼ if (n = k, x, f (n))) (m) \neq f (m)\}$
135	124 134	eqtr4d	$⊢ (((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \to \{k\} = dom ((n \in A ⟼ if (n = k, x, f (n))) ∖ f)$
136	135	unieqd	$⊢ (((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \to ⋃ \{k\} = ⋃ dom ((n \in A ⟼ if (n = k, x, f (n))) ∖ f)$
137	94 136	syl5eqr	$⊢ (((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \to k = ⋃ dom ((n \in A ⟼ if (n = k, x, f (n))) ∖ f)$
138		difeq1	$⊢ g = (n \in A ⟼ if (n = k, x, f (n))) \to g ∖ f = (n \in A ⟼ if (n = k, x, f (n))) ∖ f$
139	138	dmeqd	$⊢ g = (n \in A ⟼ if (n = k, x, f (n))) \to dom (g ∖ f) = dom ((n \in A ⟼ if (n = k, x, f (n))) ∖ f)$
140	139	unieqd	$⊢ g = (n \in A ⟼ if (n = k, x, f (n))) \to ⋃ dom (g ∖ f) = ⋃ dom ((n \in A ⟼ if (n = k, x, f (n))) ∖ f)$
141	140	rspceeqv	$⊢ ((n \in A ⟼ if (n = k, x, f (n))) \in X \land k = ⋃ dom ((n \in A ⟼ if (n = k, x, f (n))) ∖ f)) \to \exists g \in X k = ⋃ dom (g ∖ f)$
142	92 137 141	syl2anc	$⊢ (((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \to \exists g \in X k = ⋃ dom (g ∖ f)$
143	142	ex	$⊢ ((φ \land f \in X) \land k \in A) \to (x \in (⋃ F (k) ∖ \{f (k)\}) \to \exists g \in X k = ⋃ dom (g ∖ f))$
144	143	exlimdv	$⊢ ((φ \land f \in X) \land k \in A) \to (\exists x x \in (⋃ F (k) ∖ \{f (k)\}) \to \exists g \in X k = ⋃ dom (g ∖ f))$
145	70 144	syld	$⊢ ((φ \land f \in X) \land k \in A) \to (\neg ⋃ F (k) \approx 1_{𝑜} \to \exists g \in X k = ⋃ dom (g ∖ f))$
146	145	expimpd	$⊢ (φ \land f \in X) \to ((k \in A \land \neg ⋃ F (k) \approx 1_{𝑜}) \to \exists g \in X k = ⋃ dom (g ∖ f))$
147	23	breq1d	$⊢ n = k \to (⋃ F (n) \approx 1_{𝑜} \leftrightarrow ⋃ F (k) \approx 1_{𝑜})$
148	147	notbid	$⊢ n = k \to (\neg ⋃ F (n) \approx 1_{𝑜} \leftrightarrow \neg ⋃ F (k) \approx 1_{𝑜})$
149	148	elrab	$⊢ k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \leftrightarrow (k \in A \land \neg ⋃ F (k) \approx 1_{𝑜})$
150	44	elrnmpt	$⊢ k \in V \to (k \in ran (g \in X ⟼ ⋃ dom (g ∖ f)) \leftrightarrow \exists g \in X k = ⋃ dom (g ∖ f))$
151	150	elv	$⊢ k \in ran (g \in X ⟼ ⋃ dom (g ∖ f)) \leftrightarrow \exists g \in X k = ⋃ dom (g ∖ f)$
152	146 149 151	3imtr4g	$⊢ (φ \land f \in X) \to (k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \to k \in ran (g \in X ⟼ ⋃ dom (g ∖ f)))$
153	152	ssrdv	$⊢ (φ \land f \in X) \to \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \subseteq ran (g \in X ⟼ ⋃ dom (g ∖ f))$
154		ssnum	$⊢ (ran (g \in X ⟼ ⋃ dom (g ∖ f)) \in dom card \land \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \subseteq ran (g \in X ⟼ ⋃ dom (g ∖ f))) \to \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \in dom card$
155	50 153 154	syl2anc	$⊢ (φ \land f \in X) \to \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \in dom card$
156		xpnum	$⊢ (\underset{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}{⨉} ⋃ F (k) \in dom card \land \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \in dom card) \to \underset{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}{⨉} ⋃ F (k) \times \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \in dom card$
157	36 155 156	syl2anc	$⊢ (φ \land f \in X) \to \underset{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}{⨉} ⋃ F (k) \times \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \in dom card$
158	3	adantr	$⊢ (φ \land f \in X) \to A \in V$
159		rabexg	$⊢ A \in V \to \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \in V$
160	158 159	syl	$⊢ (φ \land f \in X) \to \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \in V$
161		fvex	$⊢ F (k) \in V$
162	161	uniex	$⊢ ⋃ F (k) \in V$
163	162	rgenw	$⊢ \forall k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} ⋃ F (k) \in V$
164		iunexg	$⊢ (\{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \in V \land \forall k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} ⋃ F (k) \in V) \to ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} ⋃ F (k) \in V$
165	160 163 164	sylancl	$⊢ (φ \land f \in X) \to ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} ⋃ F (k) \in V$
166		resixp	$⊢ (\{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \subseteq A \land f \in \underset{k \in A}{⨉} ⋃ F (k)) \to {f ↾}_{\{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} \in \underset{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}{⨉} ⋃ F (k)$
167	29 54 166	sylancr	$⊢ (φ \land f \in X) \to {f ↾}_{\{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} \in \underset{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}{⨉} ⋃ F (k)$
168	167	ne0d	$⊢ (φ \land f \in X) \to \underset{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}{⨉} ⋃ F (k) \neq \emptyset$
169		ixpiunwdom	$⊢ (\{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \in V \land ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} ⋃ F (k) \in V \land \underset{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}{⨉} ⋃ F (k) \neq \emptyset) \to ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} ⋃ F (k) ≼^{*} (\underset{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}{⨉} ⋃ F (k) \times \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\})$
170	160 165 168 169	syl3anc	$⊢ (φ \land f \in X) \to ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} ⋃ F (k) ≼^{*} (\underset{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}{⨉} ⋃ F (k) \times \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\})$
171		numwdom	$⊢ (\underset{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}{⨉} ⋃ F (k) \times \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \in dom card \land ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} ⋃ F (k) ≼^{*} (\underset{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}{⨉} ⋃ F (k) \times \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\})) \to ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} ⋃ F (k) \in dom card$
172	157 170 171	syl2anc	$⊢ (φ \land f \in X) \to ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} ⋃ F (k) \in dom card$
173	21 172	exlimddv	$⊢ φ \to ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} ⋃ F (k) \in dom card$

Metamath Proof Explorer

Theorem ptcmplem2

Proof