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

Metamath Proof Explorer

Theorem disjinfi

Proof