disjinfi

Description: Only a finite number of disjoint sets can have a nonempty intersection with a finite set C . (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	disjinfi.b	$⊢ (φ \land x \in A) \to B \in V$
	disjinfi.d	$⊢ φ \to \underset{x \in A}{Disj} B$
	disjinfi.c	$⊢ φ \to C \in Fin$
Assertion	disjinfi	$⊢ φ \to \{x \in A \| B \cap C \neq \emptyset\} \in Fin$

Proof

Step	Hyp	Ref	Expression
1		disjinfi.b	$⊢ (φ \land x \in A) \to B \in V$
2		disjinfi.d	$⊢ φ \to \underset{x \in A}{Disj} B$
3		disjinfi.c	$⊢ φ \to C \in Fin$
4		inss2	$⊢ ⋃ ran (x \in A ⟼ B) \cap C \subseteq C$
5		ssfi	$⊢ (C \in Fin \land ⋃ ran (x \in A ⟼ B) \cap C \subseteq C) \to ⋃ ran (x \in A ⟼ B) \cap C \in Fin$
6	3 4 5	sylancl	$⊢ φ \to ⋃ ran (x \in A ⟼ B) \cap C \in Fin$
7	4	a1i	$⊢ φ \to ⋃ ran (x \in A ⟼ B) \cap C \subseteq C$
8	3 7	ssexd	$⊢ φ \to ⋃ ran (x \in A ⟼ B) \cap C \in V$
9		elinel1	$⊢ y \in (⋃ ran (x \in A ⟼ B) \cap C) \to y \in ⋃ ran (x \in A ⟼ B)$
10		eluni2	$⊢ y \in ⋃ ran (x \in A ⟼ B) \leftrightarrow \exists w \in ran (x \in A ⟼ B) y \in w$
11	10	biimpi	$⊢ y \in ⋃ ran (x \in A ⟼ B) \to \exists w \in ran (x \in A ⟼ B) y \in w$
12		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
13	12	elrnmpt	$⊢ w \in V \to (w \in ran (x \in A ⟼ B) \leftrightarrow \exists x \in A w = B)$
14	13	elv	$⊢ w \in ran (x \in A ⟼ B) \leftrightarrow \exists x \in A w = B$
15	14	birani	$⊢ (w \in ran (x \in A ⟼ B) \land y \in w) \to \exists x \in A w = B$
16		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
17	16	nfrn	$⊢ \underline{Ⅎ} x ran (x \in A ⟼ B)$
18	17	nfcri	$⊢ Ⅎ x w \in ran (x \in A ⟼ B)$
19		nfv	$⊢ Ⅎ x y \in w$
20	18 19	nfan	$⊢ Ⅎ x (w \in ran (x \in A ⟼ B) \land y \in w)$
21		simpl	$⊢ (y \in w \land w = B) \to y \in w$
22		simpr	$⊢ (y \in w \land w = B) \to w = B$
23	21 22	eleqtrd	$⊢ (y \in w \land w = B) \to y \in B$
24	23	ex	$⊢ y \in w \to (w = B \to y \in B)$
25	24	a1d	$⊢ y \in w \to (x \in A \to (w = B \to y \in B))$
26	25	adantl	$⊢ (w \in ran (x \in A ⟼ B) \land y \in w) \to (x \in A \to (w = B \to y \in B))$
27	20 26	reximdai	$⊢ (w \in ran (x \in A ⟼ B) \land y \in w) \to (\exists x \in A w = B \to \exists x \in A y \in B)$
28	15 27	mpd	$⊢ (w \in ran (x \in A ⟼ B) \land y \in w) \to \exists x \in A y \in B$
29	28	ex	$⊢ w \in ran (x \in A ⟼ B) \to (y \in w \to \exists x \in A y \in B)$
30	29	a1i	$⊢ y \in ⋃ ran (x \in A ⟼ B) \to (w \in ran (x \in A ⟼ B) \to (y \in w \to \exists x \in A y \in B))$
31	30	rexlimdv	$⊢ y \in ⋃ ran (x \in A ⟼ B) \to (\exists w \in ran (x \in A ⟼ B) y \in w \to \exists x \in A y \in B)$
32	11 31	mpd	$⊢ y \in ⋃ ran (x \in A ⟼ B) \to \exists x \in A y \in B$
33	9 32	syl	$⊢ y \in (⋃ ran (x \in A ⟼ B) \cap C) \to \exists x \in A y \in B$
34	33	adantl	$⊢ (φ \land y \in (⋃ ran (x \in A ⟼ B) \cap C)) \to \exists x \in A y \in B$
35		nfv	$⊢ Ⅎ x φ$
36	17	nfuni	$⊢ \underline{Ⅎ} x ⋃ ran (x \in A ⟼ B)$
37		nfcv	$⊢ \underline{Ⅎ} x C$
38	36 37	nfin	$⊢ \underline{Ⅎ} x (⋃ ran (x \in A ⟼ B) \cap C)$
39	38	nfcri	$⊢ Ⅎ x y \in (⋃ ran (x \in A ⟼ B) \cap C)$
40	35 39	nfan	$⊢ Ⅎ x (φ \land y \in (⋃ ran (x \in A ⟼ B) \cap C))$
41		nfre1	$⊢ Ⅎ x \exists x \in A y \in (B \cap C)$
42		elinel2	$⊢ y \in (⋃ ran (x \in A ⟼ B) \cap C) \to y \in C$
43		simp2	$⊢ (y \in C \land x \in A \land y \in B) \to x \in A$
44		simpr	$⊢ (y \in C \land y \in B) \to y \in B$
45		simpl	$⊢ (y \in C \land y \in B) \to y \in C$
46	44 45	elind	$⊢ (y \in C \land y \in B) \to y \in (B \cap C)$
47		rspe	$⊢ (x \in A \land y \in (B \cap C)) \to \exists x \in A y \in (B \cap C)$
48	43 46 47	3imp3i2an	$⊢ (y \in C \land x \in A \land y \in B) \to \exists x \in A y \in (B \cap C)$
49	48	3exp	$⊢ y \in C \to (x \in A \to (y \in B \to \exists x \in A y \in (B \cap C)))$
50	42 49	syl	$⊢ y \in (⋃ ran (x \in A ⟼ B) \cap C) \to (x \in A \to (y \in B \to \exists x \in A y \in (B \cap C)))$
51	50	adantl	$⊢ (φ \land y \in (⋃ ran (x \in A ⟼ B) \cap C)) \to (x \in A \to (y \in B \to \exists x \in A y \in (B \cap C)))$
52	40 41 51	rexlimd	$⊢ (φ \land y \in (⋃ ran (x \in A ⟼ B) \cap C)) \to (\exists x \in A y \in B \to \exists x \in A y \in (B \cap C))$
53	34 52	mpd	$⊢ (φ \land y \in (⋃ ran (x \in A ⟼ B) \cap C)) \to \exists x \in A y \in (B \cap C)$
54		disjors	$⊢ \underset{x \in A}{Disj} B \leftrightarrow \forall z \in A \forall w \in A (z = w \lor ⦋ z / x ⦌ B \cap ⦋ w / x ⦌ B = \emptyset)$
55	2 54	sylib	$⊢ φ \to \forall z \in A \forall w \in A (z = w \lor ⦋ z / x ⦌ B \cap ⦋ w / x ⦌ B = \emptyset)$
56		nfv	$⊢ Ⅎ z \forall w \in A (x = w \lor B \cap ⦋ w / x ⦌ B = \emptyset)$
57		nfcv	$⊢ \underline{Ⅎ} x A$
58		nfv	$⊢ Ⅎ x z = w$
59		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ z / x ⦌ B$
60		nfcv	$⊢ \underline{Ⅎ} x w$
61	60	nfcsb1	$⊢ \underline{Ⅎ} x ⦋ w / x ⦌ B$
62	59 61	nfin	$⊢ \underline{Ⅎ} x (⦋ z / x ⦌ B \cap ⦋ w / x ⦌ B)$
63	62	nfeq1	$⊢ Ⅎ x ⦋ z / x ⦌ B \cap ⦋ w / x ⦌ B = \emptyset$
64	58 63	nfor	$⊢ Ⅎ x (z = w \lor ⦋ z / x ⦌ B \cap ⦋ w / x ⦌ B = \emptyset)$
65	57 64	nfralw	$⊢ Ⅎ x \forall w \in A (z = w \lor ⦋ z / x ⦌ B \cap ⦋ w / x ⦌ B = \emptyset)$
66		equequ1	$⊢ x = z \to (x = w \leftrightarrow z = w)$
67		csbeq1a	$⊢ x = z \to B = ⦋ z / x ⦌ B$
68	67	ineq1d	$⊢ x = z \to B \cap ⦋ w / x ⦌ B = ⦋ z / x ⦌ B \cap ⦋ w / x ⦌ B$
69	68	eqeq1d	$⊢ x = z \to (B \cap ⦋ w / x ⦌ B = \emptyset \leftrightarrow ⦋ z / x ⦌ B \cap ⦋ w / x ⦌ B = \emptyset)$
70	66 69	orbi12d	$⊢ x = z \to ((x = w \lor B \cap ⦋ w / x ⦌ B = \emptyset) \leftrightarrow (z = w \lor ⦋ z / x ⦌ B \cap ⦋ w / x ⦌ B = \emptyset))$
71	70	ralbidv	$⊢ x = z \to (\forall w \in A (x = w \lor B \cap ⦋ w / x ⦌ B = \emptyset) \leftrightarrow \forall w \in A (z = w \lor ⦋ z / x ⦌ B \cap ⦋ w / x ⦌ B = \emptyset))$
72	56 65 71	cbvralw	$⊢ \forall x \in A \forall w \in A (x = w \lor B \cap ⦋ w / x ⦌ B = \emptyset) \leftrightarrow \forall z \in A \forall w \in A (z = w \lor ⦋ z / x ⦌ B \cap ⦋ w / x ⦌ B = \emptyset)$
73	55 72	sylibr	$⊢ φ \to \forall x \in A \forall w \in A (x = w \lor B \cap ⦋ w / x ⦌ B = \emptyset)$
74	73	r19.21bi	$⊢ (φ \land x \in A) \to \forall w \in A (x = w \lor B \cap ⦋ w / x ⦌ B = \emptyset)$
75		rspa	$⊢ (\forall w \in A (x = w \lor B \cap ⦋ w / x ⦌ B = \emptyset) \land w \in A) \to (x = w \lor B \cap ⦋ w / x ⦌ B = \emptyset)$
76	75	orcomd	$⊢ (\forall w \in A (x = w \lor B \cap ⦋ w / x ⦌ B = \emptyset) \land w \in A) \to (B \cap ⦋ w / x ⦌ B = \emptyset \lor x = w)$
77	74 76	sylan	$⊢ ((φ \land x \in A) \land w \in A) \to (B \cap ⦋ w / x ⦌ B = \emptyset \lor x = w)$
78		elinel1	$⊢ y \in (B \cap C) \to y \in B$
79		sbsbc	$⊢ [w/ x] y \in (B \cap C) \leftrightarrow \underset{˙}{[} w / x \underset{˙}{]} y \in (B \cap C)$
80		sbcel2	$⊢ \underset{˙}{[} w / x \underset{˙}{]} y \in (B \cap C) \leftrightarrow y \in ⦋ w / x ⦌ (B \cap C)$
81		csbin	$⊢ ⦋ w / x ⦌ (B \cap C) = ⦋ w / x ⦌ B \cap ⦋ w / x ⦌ C$
82	81	eleq2i	$⊢ y \in ⦋ w / x ⦌ (B \cap C) \leftrightarrow y \in (⦋ w / x ⦌ B \cap ⦋ w / x ⦌ C)$
83	79 80 82	3bitri	$⊢ [w/ x] y \in (B \cap C) \leftrightarrow y \in (⦋ w / x ⦌ B \cap ⦋ w / x ⦌ C)$
84		elinel1	$⊢ y \in (⦋ w / x ⦌ B \cap ⦋ w / x ⦌ C) \to y \in ⦋ w / x ⦌ B$
85	83 84	sylbi	$⊢ [w/ x] y \in (B \cap C) \to y \in ⦋ w / x ⦌ B$
86		inelcm	$⊢ (y \in B \land y \in ⦋ w / x ⦌ B) \to B \cap ⦋ w / x ⦌ B \neq \emptyset$
87	86	neneqd	$⊢ (y \in B \land y \in ⦋ w / x ⦌ B) \to \neg B \cap ⦋ w / x ⦌ B = \emptyset$
88	78 85 87	syl2an	$⊢ (y \in (B \cap C) \land [w/ x] y \in (B \cap C)) \to \neg B \cap ⦋ w / x ⦌ B = \emptyset$
89		pm2.53	$⊢ (B \cap ⦋ w / x ⦌ B = \emptyset \lor x = w) \to (\neg B \cap ⦋ w / x ⦌ B = \emptyset \to x = w)$
90	77 88 89	syl2im	$⊢ ((φ \land x \in A) \land w \in A) \to ((y \in (B \cap C) \land [w/ x] y \in (B \cap C)) \to x = w)$
91	90	ralrimiva	$⊢ (φ \land x \in A) \to \forall w \in A ((y \in (B \cap C) \land [w/ x] y \in (B \cap C)) \to x = w)$
92	91	ralrimiva	$⊢ φ \to \forall x \in A \forall w \in A ((y \in (B \cap C) \land [w/ x] y \in (B \cap C)) \to x = w)$
93	92	adantr	$⊢ (φ \land y \in (⋃ ran (x \in A ⟼ B) \cap C)) \to \forall x \in A \forall w \in A ((y \in (B \cap C) \land [w/ x] y \in (B \cap C)) \to x = w)$
94		reu2	$⊢ \exists! x \in A y \in (B \cap C) \leftrightarrow (\exists x \in A y \in (B \cap C) \land \forall x \in A \forall w \in A ((y \in (B \cap C) \land [w/ x] y \in (B \cap C)) \to x = w))$
95	53 93 94	sylanbrc	$⊢ (φ \land y \in (⋃ ran (x \in A ⟼ B) \cap C)) \to \exists! x \in A y \in (B \cap C)$
96		riotacl2	$⊢ \exists! x \in A y \in (B \cap C) \to (ι x \in A \| y \in (B \cap C)) \in \{x \in A \| y \in (B \cap C)\}$
97		nfriota1	$⊢ \underline{Ⅎ} x (ι x \in A \| y \in (B \cap C))$
98	97	nfcsb1	$⊢ \underline{Ⅎ} x ⦋ (ι x \in A \| y \in (B \cap C)) / x ⦌ B$
99	98 37	nfin	$⊢ \underline{Ⅎ} x (⦋ (ι x \in A \| y \in (B \cap C)) / x ⦌ B \cap C)$
100	99	nfcri	$⊢ Ⅎ x y \in (⦋ (ι x \in A \| y \in (B \cap C)) / x ⦌ B \cap C)$
101		csbeq1a	$⊢ x = (ι x \in A \| y \in (B \cap C)) \to B = ⦋ (ι x \in A \| y \in (B \cap C)) / x ⦌ B$
102	101	ineq1d	$⊢ x = (ι x \in A \| y \in (B \cap C)) \to B \cap C = ⦋ (ι x \in A \| y \in (B \cap C)) / x ⦌ B \cap C$
103	102	eleq2d	$⊢ x = (ι x \in A \| y \in (B \cap C)) \to (y \in (B \cap C) \leftrightarrow y \in (⦋ (ι x \in A \| y \in (B \cap C)) / x ⦌ B \cap C))$
104	97 57 100 103	elrabf	$⊢ (ι x \in A \| y \in (B \cap C)) \in \{x \in A \| y \in (B \cap C)\} \leftrightarrow ((ι x \in A \| y \in (B \cap C)) \in A \land y \in (⦋ (ι x \in A \| y \in (B \cap C)) / x ⦌ B \cap C))$
105	104	simplbi	$⊢ (ι x \in A \| y \in (B \cap C)) \in \{x \in A \| y \in (B \cap C)\} \to (ι x \in A \| y \in (B \cap C)) \in A$
106	104	simprbi	$⊢ (ι x \in A \| y \in (B \cap C)) \in \{x \in A \| y \in (B \cap C)\} \to y \in (⦋ (ι x \in A \| y \in (B \cap C)) / x ⦌ B \cap C)$
107	106	ne0d	$⊢ (ι x \in A \| y \in (B \cap C)) \in \{x \in A \| y \in (B \cap C)\} \to ⦋ (ι x \in A \| y \in (B \cap C)) / x ⦌ B \cap C \neq \emptyset$
108		nfcv	$⊢ \underline{Ⅎ} x \emptyset$
109	99 108	nfne	$⊢ Ⅎ x ⦋ (ι x \in A \| y \in (B \cap C)) / x ⦌ B \cap C \neq \emptyset$
110	102	neeq1d	$⊢ x = (ι x \in A \| y \in (B \cap C)) \to (B \cap C \neq \emptyset \leftrightarrow ⦋ (ι x \in A \| y \in (B \cap C)) / x ⦌ B \cap C \neq \emptyset)$
111	97 57 109 110	elrabf	$⊢ (ι x \in A \| y \in (B \cap C)) \in \{x \in A \| B \cap C \neq \emptyset\} \leftrightarrow ((ι x \in A \| y \in (B \cap C)) \in A \land ⦋ (ι x \in A \| y \in (B \cap C)) / x ⦌ B \cap C \neq \emptyset)$
112	105 107 111	sylanbrc	$⊢ (ι x \in A \| y \in (B \cap C)) \in \{x \in A \| y \in (B \cap C)\} \to (ι x \in A \| y \in (B \cap C)) \in \{x \in A \| B \cap C \neq \emptyset\}$
113	95 96 112	3syl	$⊢ (φ \land y \in (⋃ ran (x \in A ⟼ B) \cap C)) \to (ι x \in A \| y \in (B \cap C)) \in \{x \in A \| B \cap C \neq \emptyset\}$
114	113	ralrimiva	$⊢ φ \to \forall y \in (⋃ ran (x \in A ⟼ B) \cap C) (ι x \in A \| y \in (B \cap C)) \in \{x \in A \| B \cap C \neq \emptyset\}$
115	61 37	nfin	$⊢ \underline{Ⅎ} x (⦋ w / x ⦌ B \cap C)$
116	115 108	nfne	$⊢ Ⅎ x ⦋ w / x ⦌ B \cap C \neq \emptyset$
117		csbeq1a	$⊢ x = w \to B = ⦋ w / x ⦌ B$
118	117	ineq1d	$⊢ x = w \to B \cap C = ⦋ w / x ⦌ B \cap C$
119	118	neeq1d	$⊢ x = w \to (B \cap C \neq \emptyset \leftrightarrow ⦋ w / x ⦌ B \cap C \neq \emptyset)$
120	60 57 116 119	elrabf	$⊢ w \in \{x \in A \| B \cap C \neq \emptyset\} \leftrightarrow (w \in A \land ⦋ w / x ⦌ B \cap C \neq \emptyset)$
121	120	simprbi	$⊢ w \in \{x \in A \| B \cap C \neq \emptyset\} \to ⦋ w / x ⦌ B \cap C \neq \emptyset$
122		n0	$⊢ ⦋ w / x ⦌ B \cap C \neq \emptyset \leftrightarrow \exists y y \in (⦋ w / x ⦌ B \cap C)$
123	121 122	sylib	$⊢ w \in \{x \in A \| B \cap C \neq \emptyset\} \to \exists y y \in (⦋ w / x ⦌ B \cap C)$
124	123	adantl	$⊢ (φ \land w \in \{x \in A \| B \cap C \neq \emptyset\}) \to \exists y y \in (⦋ w / x ⦌ B \cap C)$
125	120	simplbi	$⊢ w \in \{x \in A \| B \cap C \neq \emptyset\} \to w \in A$
126		elinel1	$⊢ y \in (⦋ w / x ⦌ B \cap C) \to y \in ⦋ w / x ⦌ B$
127	126	adantl	$⊢ ((φ \land w \in A) \land y \in (⦋ w / x ⦌ B \cap C)) \to y \in ⦋ w / x ⦌ B$
128		simplr	$⊢ ((φ \land w \in A) \land y \in (⦋ w / x ⦌ B \cap C)) \to w \in A$
129		nfv	$⊢ Ⅎ x (φ \land w \in A)$
130	61	nfel1	$⊢ Ⅎ x ⦋ w / x ⦌ B \in V$
131	129 130	nfim	$⊢ Ⅎ x ((φ \land w \in A) \to ⦋ w / x ⦌ B \in V)$
132		eleq1w	$⊢ x = w \to (x \in A \leftrightarrow w \in A)$
133	132	anbi2d	$⊢ x = w \to ((φ \land x \in A) \leftrightarrow (φ \land w \in A))$
134	117	eleq1d	$⊢ x = w \to (B \in V \leftrightarrow ⦋ w / x ⦌ B \in V)$
135	133 134	imbi12d	$⊢ x = w \to (((φ \land x \in A) \to B \in V) \leftrightarrow ((φ \land w \in A) \to ⦋ w / x ⦌ B \in V))$
136	131 135 1	chvarfv	$⊢ (φ \land w \in A) \to ⦋ w / x ⦌ B \in V$
137	136	adantr	$⊢ ((φ \land w \in A) \land y \in (⦋ w / x ⦌ B \cap C)) \to ⦋ w / x ⦌ B \in V$
138		eqid	$⊢ (w \in A ⟼ ⦋ w / x ⦌ B) = (w \in A ⟼ ⦋ w / x ⦌ B)$
139	138	elrnmpt1	$⊢ (w \in A \land ⦋ w / x ⦌ B \in V) \to ⦋ w / x ⦌ B \in ran (w \in A ⟼ ⦋ w / x ⦌ B)$
140	128 137 139	syl2anc	$⊢ ((φ \land w \in A) \land y \in (⦋ w / x ⦌ B \cap C)) \to ⦋ w / x ⦌ B \in ran (w \in A ⟼ ⦋ w / x ⦌ B)$
141		nfcv	$⊢ \underline{Ⅎ} w B$
142	117	equcoms	$⊢ w = x \to B = ⦋ w / x ⦌ B$
143	142	eqcomd	$⊢ w = x \to ⦋ w / x ⦌ B = B$
144	61 141 143	cbvmpt	$⊢ (w \in A ⟼ ⦋ w / x ⦌ B) = (x \in A ⟼ B)$
145	144	rneqi	$⊢ ran (w \in A ⟼ ⦋ w / x ⦌ B) = ran (x \in A ⟼ B)$
146	140 145	eleqtrdi	$⊢ ((φ \land w \in A) \land y \in (⦋ w / x ⦌ B \cap C)) \to ⦋ w / x ⦌ B \in ran (x \in A ⟼ B)$
147		elunii	$⊢ (y \in ⦋ w / x ⦌ B \land ⦋ w / x ⦌ B \in ran (x \in A ⟼ B)) \to y \in ⋃ ran (x \in A ⟼ B)$
148	127 146 147	syl2anc	$⊢ ((φ \land w \in A) \land y \in (⦋ w / x ⦌ B \cap C)) \to y \in ⋃ ran (x \in A ⟼ B)$
149		elinel2	$⊢ y \in (⦋ w / x ⦌ B \cap C) \to y \in C$
150	149	adantl	$⊢ ((φ \land w \in A) \land y \in (⦋ w / x ⦌ B \cap C)) \to y \in C$
151	148 150	elind	$⊢ ((φ \land w \in A) \land y \in (⦋ w / x ⦌ B \cap C)) \to y \in (⋃ ran (x \in A ⟼ B) \cap C)$
152		nfv	$⊢ Ⅎ w y \in (B \cap C)$
153	115	nfcri	$⊢ Ⅎ x y \in (⦋ w / x ⦌ B \cap C)$
154	118	eleq2d	$⊢ x = w \to (y \in (B \cap C) \leftrightarrow y \in (⦋ w / x ⦌ B \cap C))$
155	152 153 154	cbvriotaw	$⊢ (ι x \in A \| y \in (B \cap C)) = (ι w \in A \| y \in (⦋ w / x ⦌ B \cap C))$
156		simpr	$⊢ ((φ \land w \in A) \land y \in (⦋ w / x ⦌ B \cap C)) \to y \in (⦋ w / x ⦌ B \cap C)$
157		rspe	$⊢ (w \in A \land y \in (⦋ w / x ⦌ B \cap C)) \to \exists w \in A y \in (⦋ w / x ⦌ B \cap C)$
158	157	adantll	$⊢ ((φ \land w \in A) \land y \in (⦋ w / x ⦌ B \cap C)) \to \exists w \in A y \in (⦋ w / x ⦌ B \cap C)$
159		simpll	$⊢ ((φ \land w \in A) \land y \in (⦋ w / x ⦌ B \cap C)) \to φ$
160		sbequ	$⊢ w = z \to ([w/ x] y \in (B \cap C) \leftrightarrow [z/ x] y \in (B \cap C))$
161		sbsbc	$⊢ [z/ x] y \in (B \cap C) \leftrightarrow \underset{˙}{[} z / x \underset{˙}{]} y \in (B \cap C)$
162	161	a1i	$⊢ w = z \to ([z/ x] y \in (B \cap C) \leftrightarrow \underset{˙}{[} z / x \underset{˙}{]} y \in (B \cap C))$
163		sbcel2	$⊢ \underset{˙}{[} z / x \underset{˙}{]} y \in (B \cap C) \leftrightarrow y \in ⦋ z / x ⦌ (B \cap C)$
164		csbin	$⊢ ⦋ z / x ⦌ (B \cap C) = ⦋ z / x ⦌ B \cap ⦋ z / x ⦌ C$
165		csbconstg	$⊢ z \in V \to ⦋ z / x ⦌ C = C$
166	165	elv	$⊢ ⦋ z / x ⦌ C = C$
167	166	ineq2i	$⊢ ⦋ z / x ⦌ B \cap ⦋ z / x ⦌ C = ⦋ z / x ⦌ B \cap C$
168	164 167	eqtri	$⊢ ⦋ z / x ⦌ (B \cap C) = ⦋ z / x ⦌ B \cap C$
169	168	eleq2i	$⊢ y \in ⦋ z / x ⦌ (B \cap C) \leftrightarrow y \in (⦋ z / x ⦌ B \cap C)$
170	163 169	bitri	$⊢ \underset{˙}{[} z / x \underset{˙}{]} y \in (B \cap C) \leftrightarrow y \in (⦋ z / x ⦌ B \cap C)$
171	170	a1i	$⊢ w = z \to (\underset{˙}{[} z / x \underset{˙}{]} y \in (B \cap C) \leftrightarrow y \in (⦋ z / x ⦌ B \cap C))$
172	160 162 171	3bitrd	$⊢ w = z \to ([w/ x] y \in (B \cap C) \leftrightarrow y \in (⦋ z / x ⦌ B \cap C))$
173	172	anbi2d	$⊢ w = z \to ((y \in (B \cap C) \land [w/ x] y \in (B \cap C)) \leftrightarrow (y \in (B \cap C) \land y \in (⦋ z / x ⦌ B \cap C)))$
174		equequ2	$⊢ w = z \to (x = w \leftrightarrow x = z)$
175	173 174	imbi12d	$⊢ w = z \to (((y \in (B \cap C) \land [w/ x] y \in (B \cap C)) \to x = w) \leftrightarrow ((y \in (B \cap C) \land y \in (⦋ z / x ⦌ B \cap C)) \to x = z))$
176	175	cbvralvw	$⊢ \forall w \in A ((y \in (B \cap C) \land [w/ x] y \in (B \cap C)) \to x = w) \leftrightarrow \forall z \in A ((y \in (B \cap C) \land y \in (⦋ z / x ⦌ B \cap C)) \to x = z)$
177	176	ralbii	$⊢ \forall x \in A \forall w \in A ((y \in (B \cap C) \land [w/ x] y \in (B \cap C)) \to x = w) \leftrightarrow \forall x \in A \forall z \in A ((y \in (B \cap C) \land y \in (⦋ z / x ⦌ B \cap C)) \to x = z)$
178		nfv	$⊢ Ⅎ w \forall z \in A ((y \in (B \cap C) \land y \in (⦋ z / x ⦌ B \cap C)) \to x = z)$
179	59 37	nfin	$⊢ \underline{Ⅎ} x (⦋ z / x ⦌ B \cap C)$
180	179	nfcri	$⊢ Ⅎ x y \in (⦋ z / x ⦌ B \cap C)$
181	153 180	nfan	$⊢ Ⅎ x (y \in (⦋ w / x ⦌ B \cap C) \land y \in (⦋ z / x ⦌ B \cap C))$
182		nfv	$⊢ Ⅎ x w = z$
183	181 182	nfim	$⊢ Ⅎ x ((y \in (⦋ w / x ⦌ B \cap C) \land y \in (⦋ z / x ⦌ B \cap C)) \to w = z)$
184	57 183	nfralw	$⊢ Ⅎ x \forall z \in A ((y \in (⦋ w / x ⦌ B \cap C) \land y \in (⦋ z / x ⦌ B \cap C)) \to w = z)$
185	154	anbi1d	$⊢ x = w \to ((y \in (B \cap C) \land y \in (⦋ z / x ⦌ B \cap C)) \leftrightarrow (y \in (⦋ w / x ⦌ B \cap C) \land y \in (⦋ z / x ⦌ B \cap C)))$
186		equequ1	$⊢ x = w \to (x = z \leftrightarrow w = z)$
187	185 186	imbi12d	$⊢ x = w \to (((y \in (B \cap C) \land y \in (⦋ z / x ⦌ B \cap C)) \to x = z) \leftrightarrow ((y \in (⦋ w / x ⦌ B \cap C) \land y \in (⦋ z / x ⦌ B \cap C)) \to w = z))$
188	187	ralbidv	$⊢ x = w \to (\forall z \in A ((y \in (B \cap C) \land y \in (⦋ z / x ⦌ B \cap C)) \to x = z) \leftrightarrow \forall z \in A ((y \in (⦋ w / x ⦌ B \cap C) \land y \in (⦋ z / x ⦌ B \cap C)) \to w = z))$
189	178 184 188	cbvralw	$⊢ \forall x \in A \forall z \in A ((y \in (B \cap C) \land y \in (⦋ z / x ⦌ B \cap C)) \to x = z) \leftrightarrow \forall w \in A \forall z \in A ((y \in (⦋ w / x ⦌ B \cap C) \land y \in (⦋ z / x ⦌ B \cap C)) \to w = z)$
190		sbsbc	$⊢ [z/ w] y \in (⦋ w / x ⦌ B \cap C) \leftrightarrow \underset{˙}{[} z / w \underset{˙}{]} y \in (⦋ w / x ⦌ B \cap C)$
191		sbcel2	$⊢ \underset{˙}{[} z / w \underset{˙}{]} y \in (⦋ w / x ⦌ B \cap C) \leftrightarrow y \in ⦋ z / w ⦌ (⦋ w / x ⦌ B \cap C)$
192		csbin	$⊢ ⦋ z / w ⦌ (⦋ w / x ⦌ B \cap C) = ⦋ z / w ⦌ ⦋ w / x ⦌ B \cap ⦋ z / w ⦌ C$
193		csbcow	$⊢ ⦋ z / w ⦌ ⦋ w / x ⦌ B = ⦋ z / x ⦌ B$
194		csbconstg	$⊢ z \in V \to ⦋ z / w ⦌ C = C$
195	194	elv	$⊢ ⦋ z / w ⦌ C = C$
196	193 195	ineq12i	$⊢ ⦋ z / w ⦌ ⦋ w / x ⦌ B \cap ⦋ z / w ⦌ C = ⦋ z / x ⦌ B \cap C$
197	192 196	eqtri	$⊢ ⦋ z / w ⦌ (⦋ w / x ⦌ B \cap C) = ⦋ z / x ⦌ B \cap C$
198	197	eleq2i	$⊢ y \in ⦋ z / w ⦌ (⦋ w / x ⦌ B \cap C) \leftrightarrow y \in (⦋ z / x ⦌ B \cap C)$
199	190 191 198	3bitrri	$⊢ y \in (⦋ z / x ⦌ B \cap C) \leftrightarrow [z/ w] y \in (⦋ w / x ⦌ B \cap C)$
200	199	anbi2i	$⊢ (y \in (⦋ w / x ⦌ B \cap C) \land y \in (⦋ z / x ⦌ B \cap C)) \leftrightarrow (y \in (⦋ w / x ⦌ B \cap C) \land [z/ w] y \in (⦋ w / x ⦌ B \cap C))$
201	200	imbi1i	$⊢ ((y \in (⦋ w / x ⦌ B \cap C) \land y \in (⦋ z / x ⦌ B \cap C)) \to w = z) \leftrightarrow ((y \in (⦋ w / x ⦌ B \cap C) \land [z/ w] y \in (⦋ w / x ⦌ B \cap C)) \to w = z)$
202	201	2ralbii	$⊢ \forall w \in A \forall z \in A ((y \in (⦋ w / x ⦌ B \cap C) \land y \in (⦋ z / x ⦌ B \cap C)) \to w = z) \leftrightarrow \forall w \in A \forall z \in A ((y \in (⦋ w / x ⦌ B \cap C) \land [z/ w] y \in (⦋ w / x ⦌ B \cap C)) \to w = z)$
203	177 189 202	3bitri	$⊢ \forall x \in A \forall w \in A ((y \in (B \cap C) \land [w/ x] y \in (B \cap C)) \to x = w) \leftrightarrow \forall w \in A \forall z \in A ((y \in (⦋ w / x ⦌ B \cap C) \land [z/ w] y \in (⦋ w / x ⦌ B \cap C)) \to w = z)$
204	93 203	sylib	$⊢ (φ \land y \in (⋃ ran (x \in A ⟼ B) \cap C)) \to \forall w \in A \forall z \in A ((y \in (⦋ w / x ⦌ B \cap C) \land [z/ w] y \in (⦋ w / x ⦌ B \cap C)) \to w = z)$
205	159 151 204	syl2anc	$⊢ ((φ \land w \in A) \land y \in (⦋ w / x ⦌ B \cap C)) \to \forall w \in A \forall z \in A ((y \in (⦋ w / x ⦌ B \cap C) \land [z/ w] y \in (⦋ w / x ⦌ B \cap C)) \to w = z)$
206		reu2	$⊢ \exists! w \in A y \in (⦋ w / x ⦌ B \cap C) \leftrightarrow (\exists w \in A y \in (⦋ w / x ⦌ B \cap C) \land \forall w \in A \forall z \in A ((y \in (⦋ w / x ⦌ B \cap C) \land [z/ w] y \in (⦋ w / x ⦌ B \cap C)) \to w = z))$
207	158 205 206	sylanbrc	$⊢ ((φ \land w \in A) \land y \in (⦋ w / x ⦌ B \cap C)) \to \exists! w \in A y \in (⦋ w / x ⦌ B \cap C)$
208		riota1	$⊢ \exists! w \in A y \in (⦋ w / x ⦌ B \cap C) \to ((w \in A \land y \in (⦋ w / x ⦌ B \cap C)) \leftrightarrow (ι w \in A \| y \in (⦋ w / x ⦌ B \cap C)) = w)$
209	207 208	syl	$⊢ ((φ \land w \in A) \land y \in (⦋ w / x ⦌ B \cap C)) \to ((w \in A \land y \in (⦋ w / x ⦌ B \cap C)) \leftrightarrow (ι w \in A \| y \in (⦋ w / x ⦌ B \cap C)) = w)$
210	128 156 209	mpbi2and	$⊢ ((φ \land w \in A) \land y \in (⦋ w / x ⦌ B \cap C)) \to (ι w \in A \| y \in (⦋ w / x ⦌ B \cap C)) = w$
211	155 210	eqtr2id	$⊢ ((φ \land w \in A) \land y \in (⦋ w / x ⦌ B \cap C)) \to w = (ι x \in A \| y \in (B \cap C))$
212	151 211	jca	$⊢ ((φ \land w \in A) \land y \in (⦋ w / x ⦌ B \cap C)) \to (y \in (⋃ ran (x \in A ⟼ B) \cap C) \land w = (ι x \in A \| y \in (B \cap C)))$
213	212	ex	$⊢ (φ \land w \in A) \to (y \in (⦋ w / x ⦌ B \cap C) \to (y \in (⋃ ran (x \in A ⟼ B) \cap C) \land w = (ι x \in A \| y \in (B \cap C))))$
214	125 213	sylan2	$⊢ (φ \land w \in \{x \in A \| B \cap C \neq \emptyset\}) \to (y \in (⦋ w / x ⦌ B \cap C) \to (y \in (⋃ ran (x \in A ⟼ B) \cap C) \land w = (ι x \in A \| y \in (B \cap C))))$
215	214	eximdv	$⊢ (φ \land w \in \{x \in A \| B \cap C \neq \emptyset\}) \to (\exists y y \in (⦋ w / x ⦌ B \cap C) \to \exists y (y \in (⋃ ran (x \in A ⟼ B) \cap C) \land w = (ι x \in A \| y \in (B \cap C))))$
216	124 215	mpd	$⊢ (φ \land w \in \{x \in A \| B \cap C \neq \emptyset\}) \to \exists y (y \in (⋃ ran (x \in A ⟼ B) \cap C) \land w = (ι x \in A \| y \in (B \cap C)))$
217		df-rex	$⊢ \exists y \in (⋃ ran (x \in A ⟼ B) \cap C) w = (ι x \in A \| y \in (B \cap C)) \leftrightarrow \exists y (y \in (⋃ ran (x \in A ⟼ B) \cap C) \land w = (ι x \in A \| y \in (B \cap C)))$
218	216 217	sylibr	$⊢ (φ \land w \in \{x \in A \| B \cap C \neq \emptyset\}) \to \exists y \in (⋃ ran (x \in A ⟼ B) \cap C) w = (ι x \in A \| y \in (B \cap C))$
219	218	ralrimiva	$⊢ φ \to \forall w \in \{x \in A \| B \cap C \neq \emptyset\} \exists y \in (⋃ ran (x \in A ⟼ B) \cap C) w = (ι x \in A \| y \in (B \cap C))$
220		eqid	$⊢ (y \in (⋃ ran (x \in A ⟼ B) \cap C) ⟼ (ι x \in A \| y \in (B \cap C))) = (y \in (⋃ ran (x \in A ⟼ B) \cap C) ⟼ (ι x \in A \| y \in (B \cap C)))$
221	220	fompt	$⊢ (y \in (⋃ ran (x \in A ⟼ B) \cap C) ⟼ (ι x \in A \| y \in (B \cap C))) : ⋃ ran (x \in A ⟼ B) \cap C \underset{onto}{⟶} \{x \in A \| B \cap C \neq \emptyset\} \leftrightarrow (\forall y \in (⋃ ran (x \in A ⟼ B) \cap C) (ι x \in A \| y \in (B \cap C)) \in \{x \in A \| B \cap C \neq \emptyset\} \land \forall w \in \{x \in A \| B \cap C \neq \emptyset\} \exists y \in (⋃ ran (x \in A ⟼ B) \cap C) w = (ι x \in A \| y \in (B \cap C)))$
222	114 219 221	sylanbrc	$⊢ φ \to (y \in (⋃ ran (x \in A ⟼ B) \cap C) ⟼ (ι x \in A \| y \in (B \cap C))) : ⋃ ran (x \in A ⟼ B) \cap C \underset{onto}{⟶} \{x \in A \| B \cap C \neq \emptyset\}$
223		fodomg	$⊢ ⋃ ran (x \in A ⟼ B) \cap C \in V \to ((y \in (⋃ ran (x \in A ⟼ B) \cap C) ⟼ (ι x \in A \| y \in (B \cap C))) : ⋃ ran (x \in A ⟼ B) \cap C \underset{onto}{⟶} \{x \in A \| B \cap C \neq \emptyset\} \to \{x \in A \| B \cap C \neq \emptyset\} ≼ (⋃ ran (x \in A ⟼ B) \cap C))$
224	8 222 223	sylc	$⊢ φ \to \{x \in A \| B \cap C \neq \emptyset\} ≼ (⋃ ran (x \in A ⟼ B) \cap C)$
225		domfi	$⊢ (⋃ ran (x \in A ⟼ B) \cap C \in Fin \land \{x \in A \| B \cap C \neq \emptyset\} ≼ (⋃ ran (x \in A ⟼ B) \cap C)) \to \{x \in A \| B \cap C \neq \emptyset\} \in Fin$
226	6 224 225	syl2anc	$⊢ φ \to \{x \in A \| B \cap C \neq \emptyset\} \in Fin$

Metamath Proof Explorer

Theorem disjinfi

Proof