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		0fi	$⊢ \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	eqtrdi	$⊢ 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	biimtrrid	$⊢ ((φ \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	imbitrdi	$⊢ ((φ \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		unisnv	$⊢ ⋃ \{k\} = k$
94		simplr	$⊢ (((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \to k \in A$
95		eleq1w	$⊢ m = k \to (m \in A \leftrightarrow k \in A)$
96	94 95	syl5ibrcom	$⊢ (((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \to (m = k \to m \in A)$
97	96	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))$
98		equequ1	$⊢ n = m \to (n = k \leftrightarrow m = k)$
99		fveq2	$⊢ n = m \to f (n) = f (m)$
100	98 99	ifbieq2d	$⊢ n = m \to if (n = k, x, f (n)) = if (m = k, x, f (m))$
101		eqid	$⊢ (n \in A ⟼ if (n = k, x, f (n))) = (n \in A ⟼ if (n = k, x, f (n)))$
102		vex	$⊢ x \in V$
103		fvex	$⊢ f (m) \in V$
104	102 103	ifex	$⊢ if (m = k, x, f (m)) \in V$
105	100 101 104	fvmpt	$⊢ m \in A \to (n \in A ⟼ if (n = k, x, f (n))) (m) = if (m = k, x, f (m))$
106	105	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))$
107	106	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))$
108		iffalse	$⊢ \neg m = k \to if (m = k, x, f (m)) = f (m)$
109	108	necon1ai	$⊢ if (m = k, x, f (m)) \neq f (m) \to m = k$
110		eldifsni	$⊢ x \in (⋃ F (k) ∖ \{f (k)\}) \to x \neq f (k)$
111	110	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)$
112		iftrue	$⊢ m = k \to if (m = k, x, f (m)) = x$
113		fveq2	$⊢ m = k \to f (m) = f (k)$
114	112 113	neeq12d	$⊢ m = k \to (if (m = k, x, f (m)) \neq f (m) \leftrightarrow x \neq f (k))$
115	111 114	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))$
116	109 115	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)$
117	107 116	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)$
118	117	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))$
119	97 118	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)))$
120	119	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))\}$
121		df-sn	$⊢ \{k\} = \{m \| m = k\}$
122		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))\}$
123	120 121 122	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)\}$
124		fvex	$⊢ f (n) \in V$
125	102 124	ifex	$⊢ if (n = k, x, f (n)) \in V$
126	125	rgenw	$⊢ \forall n \in A if (n = k, x, f (n)) \in V$
127	101	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$
128	126 127	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$
129		ixpfn	$⊢ f \in \underset{n \in A}{⨉} ⋃ F (n) \to f Fn A$
130	76 129	syl	$⊢ (φ \land f \in X) \to f Fn A$
131	130	ad2antrr	$⊢ (((φ \land f \in X) \land k \in A) \land x \in (⋃ F (k) ∖ \{f (k)\})) \to f Fn A$
132		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)\}$
133	128 131 132	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)\}$
134	123 133	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)$
135	134	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)$
136	93 135	eqtr3id	$⊢ (((φ \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		difeq1	$⊢ g = (n \in A ⟼ if (n = k, x, f (n))) \to g ∖ f = (n \in A ⟼ if (n = k, x, f (n))) ∖ f$
138	137	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)$
139	138	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)$
140	139	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)$
141	92 136 140	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)$
142	141	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))$
143	142	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))$
144	70 143	syld	$⊢ ((φ \land f \in X) \land k \in A) \to (\neg ⋃ F (k) \approx 1_{𝑜} \to \exists g \in X k = ⋃ dom (g ∖ f))$
145	144	expimpd	$⊢ (φ \land f \in X) \to ((k \in A \land \neg ⋃ F (k) \approx 1_{𝑜}) \to \exists g \in X k = ⋃ dom (g ∖ f))$
146	23	breq1d	$⊢ n = k \to (⋃ F (n) \approx 1_{𝑜} \leftrightarrow ⋃ F (k) \approx 1_{𝑜})$
147	146	notbid	$⊢ n = k \to (\neg ⋃ F (n) \approx 1_{𝑜} \leftrightarrow \neg ⋃ F (k) \approx 1_{𝑜})$
148	147	elrab	$⊢ k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \leftrightarrow (k \in A \land \neg ⋃ F (k) \approx 1_{𝑜})$
149	44	elrnmpt	$⊢ k \in V \to (k \in ran (g \in X ⟼ ⋃ dom (g ∖ f)) \leftrightarrow \exists g \in X k = ⋃ dom (g ∖ f))$
150	149	elv	$⊢ k \in ran (g \in X ⟼ ⋃ dom (g ∖ f)) \leftrightarrow \exists g \in X k = ⋃ dom (g ∖ f)$
151	145 148 150	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)))$
152	151	ssrdv	$⊢ (φ \land f \in X) \to \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \subseteq ran (g \in X ⟼ ⋃ dom (g ∖ f))$
153		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$
154	50 152 153	syl2anc	$⊢ (φ \land f \in X) \to \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \in dom card$
155		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$
156	36 154 155	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$
157	3	adantr	$⊢ (φ \land f \in X) \to A \in V$
158		rabexg	$⊢ A \in V \to \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \in V$
159	157 158	syl	$⊢ (φ \land f \in X) \to \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} \in V$
160		fvex	$⊢ F (k) \in V$
161	160	uniex	$⊢ ⋃ F (k) \in V$
162	161	rgenw	$⊢ \forall k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\} ⋃ F (k) \in V$
163		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$
164	159 162 163	sylancl	$⊢ (φ \land f \in X) \to ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} ⋃ F (k) \in V$
165		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)$
166	29 54 165	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)$
167	166	ne0d	$⊢ (φ \land f \in X) \to \underset{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}}{⨉} ⋃ F (k) \neq \emptyset$
168		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_{𝑜}\})$
169	159 164 167 168	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_{𝑜}\})$
170		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$
171	156 169 170	syl2anc	$⊢ (φ \land f \in X) \to ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} ⋃ F (k) \in dom card$
172	21 171	exlimddv	$⊢ φ \to ⋃_{k \in \{n \in A \| \neg ⋃ F (n) \approx 1_{𝑜}\}} ⋃ F (k) \in dom card$

Metamath Proof Explorer

Theorem ptcmplem2

Proof