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

Metamath Proof Explorer

Theorem disjinfi

Proof