disjinfi

Description: Only a finite number of disjoint sets can have a nonempty intersection with a finite set C . The proof uses fodomfi rather than fodomg , and so does not require ax-ac . (Contributed by Glauco Siliprandi, 17-Aug-2020) (Revised by Vincent Gonzalez, 19-Aug-2026)

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

Metamath Proof Explorer

Theorem disjinfi

Proof