disjunsn

Description: Append an element to a disjoint collection. Similar to ralunsn , gsumunsn , etc. (Contributed by Thierry Arnoux, 28-Mar-2018)

		Ref	Expression
	Hypothesis	disjunsn.s	$⊢ x = M \to B = C$
	Assertion	disjunsn	$⊢ (M \in V \land \neg M \in A) \to (\underset{x \in A \cup \{M\}}{Disj} B \leftrightarrow (\underset{x \in A}{Disj} B \land ⋃_{x \in A} B \cap C = \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		disjunsn.s	$⊢ x = M \to B = C$
2		disjors	$⊢ \underset{x \in A \cup \{M\}}{Disj} B \leftrightarrow \forall i \in (A \cup \{M\}) \forall j \in (A \cup \{M\}) (i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)$
3		eqeq1	$⊢ i = M \to (i = j \leftrightarrow M = j)$
4		csbeq1	$⊢ i = M \to ⦋ i / x ⦌ B = ⦋ M / x ⦌ B$
5	4	ineq1d	$⊢ i = M \to ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B$
6	5	eqeq1d	$⊢ i = M \to (⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset \leftrightarrow ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)$
7	3 6	orbi12d	$⊢ i = M \to ((i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \leftrightarrow (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset))$
8	7	ralbidv	$⊢ i = M \to (\forall j \in (A \cup \{M\}) (i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \leftrightarrow \forall j \in (A \cup \{M\}) (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset))$
9	8	ralunsn	$⊢ M \in V \to (\forall i \in (A \cup \{M\}) \forall j \in (A \cup \{M\}) (i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \leftrightarrow (\forall i \in A \forall j \in (A \cup \{M\}) (i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \land \forall j \in (A \cup \{M\}) (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)))$
10	2 9	syl5bb	$⊢ M \in V \to (\underset{x \in A \cup \{M\}}{Disj} B \leftrightarrow (\forall i \in A \forall j \in (A \cup \{M\}) (i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \land \forall j \in (A \cup \{M\}) (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)))$
11		eqeq2	$⊢ j = M \to (i = j \leftrightarrow i = M)$
12		csbeq1	$⊢ j = M \to ⦋ j / x ⦌ B = ⦋ M / x ⦌ B$
13	12	ineq2d	$⊢ j = M \to ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B$
14	13	eqeq1d	$⊢ j = M \to (⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset \leftrightarrow ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)$
15	11 14	orbi12d	$⊢ j = M \to ((i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \leftrightarrow (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset))$
16	15	ralunsn	$⊢ M \in V \to (\forall j \in (A \cup \{M\}) (i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \leftrightarrow (\forall j \in A (i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \land (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)))$
17	16	ralbidv	$⊢ M \in V \to (\forall i \in A \forall j \in (A \cup \{M\}) (i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \leftrightarrow \forall i \in A (\forall j \in A (i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \land (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)))$
18		eqeq2	$⊢ j = M \to (M = j \leftrightarrow M = M)$
19	12	ineq2d	$⊢ j = M \to ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = ⦋ M / x ⦌ B \cap ⦋ M / x ⦌ B$
20	19	eqeq1d	$⊢ j = M \to (⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset \leftrightarrow ⦋ M / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)$
21	18 20	orbi12d	$⊢ j = M \to ((M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \leftrightarrow (M = M \lor ⦋ M / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset))$
22	21	ralunsn	$⊢ M \in V \to (\forall j \in (A \cup \{M\}) (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \leftrightarrow (\forall j \in A (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \land (M = M \lor ⦋ M / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)))$
23		eqid	$⊢ M = M$
24	23	orci	$⊢ (M = M \lor ⦋ M / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)$
25	24	biantru	$⊢ \forall j \in A (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \leftrightarrow (\forall j \in A (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \land (M = M \lor ⦋ M / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset))$
26	22 25	bitr4di	$⊢ M \in V \to (\forall j \in (A \cup \{M\}) (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \leftrightarrow \forall j \in A (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset))$
27	17 26	anbi12d	$⊢ M \in V \to ((\forall i \in A \forall j \in (A \cup \{M\}) (i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \land \forall j \in (A \cup \{M\}) (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)) \leftrightarrow (\forall i \in A (\forall j \in A (i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \land (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)) \land \forall j \in A (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)))$
28	10 27	bitrd	$⊢ M \in V \to (\underset{x \in A \cup \{M\}}{Disj} B \leftrightarrow (\forall i \in A (\forall j \in A (i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \land (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)) \land \forall j \in A (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)))$
29		r19.26	$⊢ \forall i \in A (\forall j \in A (i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \land (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)) \leftrightarrow (\forall i \in A \forall j \in A (i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \land \forall i \in A (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset))$
30		disjors	$⊢ \underset{x \in A}{Disj} B \leftrightarrow \forall i \in A \forall j \in A (i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)$
31	30	anbi1i	$⊢ (\underset{x \in A}{Disj} B \land \forall i \in A (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)) \leftrightarrow (\forall i \in A \forall j \in A (i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \land \forall i \in A (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset))$
32	29 31	bitr4i	$⊢ \forall i \in A (\forall j \in A (i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \land (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)) \leftrightarrow (\underset{x \in A}{Disj} B \land \forall i \in A (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset))$
33	32	anbi1i	$⊢ (\forall i \in A (\forall j \in A (i = j \lor ⦋ i / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \land (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)) \land \forall j \in A (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)) \leftrightarrow ((\underset{x \in A}{Disj} B \land \forall i \in A (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)) \land \forall j \in A (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset))$
34	28 33	bitrdi	$⊢ M \in V \to (\underset{x \in A \cup \{M\}}{Disj} B \leftrightarrow ((\underset{x \in A}{Disj} B \land \forall i \in A (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)) \land \forall j \in A (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)))$
35	34	adantr	$⊢ (M \in V \land \neg M \in A) \to (\underset{x \in A \cup \{M\}}{Disj} B \leftrightarrow ((\underset{x \in A}{Disj} B \land \forall i \in A (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)) \land \forall j \in A (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)))$
36		orcom	$⊢ (⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset \lor i = M) \leftrightarrow (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)$
37	36	ralbii	$⊢ \forall i \in A (⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset \lor i = M) \leftrightarrow \forall i \in A (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)$
38		r19.30	$⊢ \forall i \in A (⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset \lor i = M) \to (\forall i \in A ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset \lor \exists i \in A i = M)$
39		risset	$⊢ M \in A \leftrightarrow \exists i \in A i = M$
40		biorf	$⊢ \neg \exists i \in A i = M \to (\forall i \in A ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset \leftrightarrow (\exists i \in A i = M \lor \forall i \in A ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset))$
41	39 40	sylnbi	$⊢ \neg M \in A \to (\forall i \in A ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset \leftrightarrow (\exists i \in A i = M \lor \forall i \in A ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset))$
42	41	adantl	$⊢ (M \in V \land \neg M \in A) \to (\forall i \in A ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset \leftrightarrow (\exists i \in A i = M \lor \forall i \in A ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset))$
43		orcom	$⊢ (\exists i \in A i = M \lor \forall i \in A ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset) \leftrightarrow (\forall i \in A ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset \lor \exists i \in A i = M)$
44	42 43	bitrdi	$⊢ (M \in V \land \neg M \in A) \to (\forall i \in A ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset \leftrightarrow (\forall i \in A ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset \lor \exists i \in A i = M))$
45	38 44	syl5ibr	$⊢ (M \in V \land \neg M \in A) \to (\forall i \in A (⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset \lor i = M) \to \forall i \in A ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)$
46	37 45	syl5bir	$⊢ (M \in V \land \neg M \in A) \to (\forall i \in A (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset) \to \forall i \in A ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)$
47		olc	$⊢ ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset \to (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)$
48	47	ralimi	$⊢ \forall i \in A ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset \to \forall i \in A (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)$
49	46 48	impbid1	$⊢ (M \in V \land \neg M \in A) \to (\forall i \in A (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset) \leftrightarrow \forall i \in A ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)$
50		nfv	$⊢ Ⅎ i B \cap C = \emptyset$
51		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ i / x ⦌ B$
52		nfcv	$⊢ \underline{Ⅎ} x C$
53	51 52	nfin	$⊢ \underline{Ⅎ} x (⦋ i / x ⦌ B \cap C)$
54	53	nfeq1	$⊢ Ⅎ x ⦋ i / x ⦌ B \cap C = \emptyset$
55		csbeq1a	$⊢ x = i \to B = ⦋ i / x ⦌ B$
56	55	ineq1d	$⊢ x = i \to B \cap C = ⦋ i / x ⦌ B \cap C$
57	56	eqeq1d	$⊢ x = i \to (B \cap C = \emptyset \leftrightarrow ⦋ i / x ⦌ B \cap C = \emptyset)$
58	50 54 57	cbvralw	$⊢ \forall x \in A B \cap C = \emptyset \leftrightarrow \forall i \in A ⦋ i / x ⦌ B \cap C = \emptyset$
59	58	a1i	$⊢ M \in V \to (\forall x \in A B \cap C = \emptyset \leftrightarrow \forall i \in A ⦋ i / x ⦌ B \cap C = \emptyset)$
60		ss0b	$⊢ ⋃_{x \in A} (B \cap C) \subseteq \emptyset \leftrightarrow ⋃_{x \in A} (B \cap C) = \emptyset$
61		iunss	$⊢ ⋃_{x \in A} (B \cap C) \subseteq \emptyset \leftrightarrow \forall x \in A B \cap C \subseteq \emptyset$
62		iunin1	$⊢ ⋃_{x \in A} (B \cap C) = ⋃_{x \in A} B \cap C$
63	62	eqeq1i	$⊢ ⋃_{x \in A} (B \cap C) = \emptyset \leftrightarrow ⋃_{x \in A} B \cap C = \emptyset$
64	60 61 63	3bitr3ri	$⊢ ⋃_{x \in A} B \cap C = \emptyset \leftrightarrow \forall x \in A B \cap C \subseteq \emptyset$
65		ss0b	$⊢ B \cap C \subseteq \emptyset \leftrightarrow B \cap C = \emptyset$
66	65	ralbii	$⊢ \forall x \in A B \cap C \subseteq \emptyset \leftrightarrow \forall x \in A B \cap C = \emptyset$
67	64 66	bitri	$⊢ ⋃_{x \in A} B \cap C = \emptyset \leftrightarrow \forall x \in A B \cap C = \emptyset$
68	67	a1i	$⊢ M \in V \to (⋃_{x \in A} B \cap C = \emptyset \leftrightarrow \forall x \in A B \cap C = \emptyset)$
69		nfcvd	$⊢ M \in V \to \underline{Ⅎ} x C$
70	69 1	csbiegf	$⊢ M \in V \to ⦋ M / x ⦌ B = C$
71	70	ineq2d	$⊢ M \in V \to ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = ⦋ i / x ⦌ B \cap C$
72	71	eqeq1d	$⊢ M \in V \to (⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset \leftrightarrow ⦋ i / x ⦌ B \cap C = \emptyset)$
73	72	ralbidv	$⊢ M \in V \to (\forall i \in A ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset \leftrightarrow \forall i \in A ⦋ i / x ⦌ B \cap C = \emptyset)$
74	59 68 73	3bitr4d	$⊢ M \in V \to (⋃_{x \in A} B \cap C = \emptyset \leftrightarrow \forall i \in A ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)$
75	74	adantr	$⊢ (M \in V \land \neg M \in A) \to (⋃_{x \in A} B \cap C = \emptyset \leftrightarrow \forall i \in A ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)$
76	49 75	bitr4d	$⊢ (M \in V \land \neg M \in A) \to (\forall i \in A (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset) \leftrightarrow ⋃_{x \in A} B \cap C = \emptyset)$
77	76	anbi2d	$⊢ (M \in V \land \neg M \in A) \to ((\underset{x \in A}{Disj} B \land \forall i \in A (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)) \leftrightarrow (\underset{x \in A}{Disj} B \land ⋃_{x \in A} B \cap C = \emptyset))$
78		orcom	$⊢ (⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset \lor M = j) \leftrightarrow (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)$
79	78	ralbii	$⊢ \forall j \in A (⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset \lor M = j) \leftrightarrow \forall j \in A (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)$
80		r19.30	$⊢ \forall j \in A (⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset \lor M = j) \to (\forall j \in A ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset \lor \exists j \in A M = j)$
81		clel5	$⊢ M \in A \leftrightarrow \exists j \in A M = j$
82		biorf	$⊢ \neg \exists j \in A M = j \to (\forall j \in A ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset \leftrightarrow (\exists j \in A M = j \lor \forall j \in A ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset))$
83	81 82	sylnbi	$⊢ \neg M \in A \to (\forall j \in A ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset \leftrightarrow (\exists j \in A M = j \lor \forall j \in A ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset))$
84	83	adantl	$⊢ (M \in V \land \neg M \in A) \to (\forall j \in A ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset \leftrightarrow (\exists j \in A M = j \lor \forall j \in A ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset))$
85		orcom	$⊢ (\exists j \in A M = j \lor \forall j \in A ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \leftrightarrow (\forall j \in A ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset \lor \exists j \in A M = j)$
86	84 85	bitrdi	$⊢ (M \in V \land \neg M \in A) \to (\forall j \in A ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset \leftrightarrow (\forall j \in A ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset \lor \exists j \in A M = j))$
87	80 86	syl5ibr	$⊢ (M \in V \land \neg M \in A) \to (\forall j \in A (⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset \lor M = j) \to \forall j \in A ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)$
88	79 87	syl5bir	$⊢ (M \in V \land \neg M \in A) \to (\forall j \in A (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \to \forall j \in A ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)$
89		olc	$⊢ ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset \to (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)$
90	89	ralimi	$⊢ \forall j \in A ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset \to \forall j \in A (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)$
91	88 90	impbid1	$⊢ (M \in V \land \neg M \in A) \to (\forall j \in A (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \leftrightarrow \forall j \in A ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)$
92		nfv	$⊢ Ⅎ j B \cap C = \emptyset$
93		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ j / x ⦌ B$
94	93 52	nfin	$⊢ \underline{Ⅎ} x (⦋ j / x ⦌ B \cap C)$
95	94	nfeq1	$⊢ Ⅎ x ⦋ j / x ⦌ B \cap C = \emptyset$
96		csbeq1a	$⊢ x = j \to B = ⦋ j / x ⦌ B$
97	96	ineq1d	$⊢ x = j \to B \cap C = ⦋ j / x ⦌ B \cap C$
98	97	eqeq1d	$⊢ x = j \to (B \cap C = \emptyset \leftrightarrow ⦋ j / x ⦌ B \cap C = \emptyset)$
99	92 95 98	cbvralw	$⊢ \forall x \in A B \cap C = \emptyset \leftrightarrow \forall j \in A ⦋ j / x ⦌ B \cap C = \emptyset$
100	99	a1i	$⊢ M \in V \to (\forall x \in A B \cap C = \emptyset \leftrightarrow \forall j \in A ⦋ j / x ⦌ B \cap C = \emptyset)$
101		incom	$⊢ ⦋ j / x ⦌ B \cap C = C \cap ⦋ j / x ⦌ B$
102	101	eqeq1i	$⊢ ⦋ j / x ⦌ B \cap C = \emptyset \leftrightarrow C \cap ⦋ j / x ⦌ B = \emptyset$
103	102	ralbii	$⊢ \forall j \in A ⦋ j / x ⦌ B \cap C = \emptyset \leftrightarrow \forall j \in A C \cap ⦋ j / x ⦌ B = \emptyset$
104	100 103	bitrdi	$⊢ M \in V \to (\forall x \in A B \cap C = \emptyset \leftrightarrow \forall j \in A C \cap ⦋ j / x ⦌ B = \emptyset)$
105	70	ineq1d	$⊢ M \in V \to ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = C \cap ⦋ j / x ⦌ B$
106	105	eqeq1d	$⊢ M \in V \to (⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset \leftrightarrow C \cap ⦋ j / x ⦌ B = \emptyset)$
107	106	ralbidv	$⊢ M \in V \to (\forall j \in A ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset \leftrightarrow \forall j \in A C \cap ⦋ j / x ⦌ B = \emptyset)$
108	104 68 107	3bitr4d	$⊢ M \in V \to (⋃_{x \in A} B \cap C = \emptyset \leftrightarrow \forall j \in A ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)$
109	108	adantr	$⊢ (M \in V \land \neg M \in A) \to (⋃_{x \in A} B \cap C = \emptyset \leftrightarrow \forall j \in A ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)$
110	91 109	bitr4d	$⊢ (M \in V \land \neg M \in A) \to (\forall j \in A (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset) \leftrightarrow ⋃_{x \in A} B \cap C = \emptyset)$
111	77 110	anbi12d	$⊢ (M \in V \land \neg M \in A) \to (((\underset{x \in A}{Disj} B \land \forall i \in A (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)) \land \forall j \in A (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)) \leftrightarrow ((\underset{x \in A}{Disj} B \land ⋃_{x \in A} B \cap C = \emptyset) \land ⋃_{x \in A} B \cap C = \emptyset))$
112		anass	$⊢ ((\underset{x \in A}{Disj} B \land ⋃_{x \in A} B \cap C = \emptyset) \land ⋃_{x \in A} B \cap C = \emptyset) \leftrightarrow (\underset{x \in A}{Disj} B \land (⋃_{x \in A} B \cap C = \emptyset \land ⋃_{x \in A} B \cap C = \emptyset))$
113		anidm	$⊢ (⋃_{x \in A} B \cap C = \emptyset \land ⋃_{x \in A} B \cap C = \emptyset) \leftrightarrow ⋃_{x \in A} B \cap C = \emptyset$
114	113	anbi2i	$⊢ (\underset{x \in A}{Disj} B \land (⋃_{x \in A} B \cap C = \emptyset \land ⋃_{x \in A} B \cap C = \emptyset)) \leftrightarrow (\underset{x \in A}{Disj} B \land ⋃_{x \in A} B \cap C = \emptyset)$
115	112 114	bitri	$⊢ ((\underset{x \in A}{Disj} B \land ⋃_{x \in A} B \cap C = \emptyset) \land ⋃_{x \in A} B \cap C = \emptyset) \leftrightarrow (\underset{x \in A}{Disj} B \land ⋃_{x \in A} B \cap C = \emptyset)$
116	111 115	bitrdi	$⊢ (M \in V \land \neg M \in A) \to (((\underset{x \in A}{Disj} B \land \forall i \in A (i = M \lor ⦋ i / x ⦌ B \cap ⦋ M / x ⦌ B = \emptyset)) \land \forall j \in A (M = j \lor ⦋ M / x ⦌ B \cap ⦋ j / x ⦌ B = \emptyset)) \leftrightarrow (\underset{x \in A}{Disj} B \land ⋃_{x \in A} B \cap C = \emptyset))$
117	35 116	bitrd	$⊢ (M \in V \land \neg M \in A) \to (\underset{x \in A \cup \{M\}}{Disj} B \leftrightarrow (\underset{x \in A}{Disj} B \land ⋃_{x \in A} B \cap C = \emptyset))$

Metamath Proof Explorer

Theorem disjunsn

Proof