saddisjlem

	Ref	Expression
Hypotheses	saddisj.1	$⊢ φ \to A \subseteq ℕ_{0}$
	saddisj.2	$⊢ φ \to B \subseteq ℕ_{0}$
	saddisj.3	$⊢ φ \to A \cap B = \emptyset$
	saddisjlem.c	$⊢ C = seq 0 ((c \in 2_{𝑜}, m \in ℕ_{0} ⟼ if (cadd (m \in A, m \in B, \emptyset \in c), 1_{𝑜}, \emptyset)), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)))$
	saddisjlem.3	$⊢ φ \to N \in ℕ_{0}$
Assertion	saddisjlem	$⊢ φ \to (N \in (A sadd B) \leftrightarrow N \in (A \cup B))$

Proof

Step	Hyp	Ref	Expression
1		saddisj.1	$⊢ φ \to A \subseteq ℕ_{0}$
2		saddisj.2	$⊢ φ \to B \subseteq ℕ_{0}$
3		saddisj.3	$⊢ φ \to A \cap B = \emptyset$
4		saddisjlem.c	$⊢ C = seq 0 ((c \in 2_{𝑜}, m \in ℕ_{0} ⟼ if (cadd (m \in A, m \in B, \emptyset \in c), 1_{𝑜}, \emptyset)), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)))$
5		saddisjlem.3	$⊢ φ \to N \in ℕ_{0}$
6	1 2 4 5	sadval	$⊢ φ \to (N \in (A sadd B) \leftrightarrow hadd (N \in A, N \in B, \emptyset \in C (N)))$
7		fveq2	$⊢ x = 0 \to C (x) = C (0)$
8	7	eleq2d	$⊢ x = 0 \to (\emptyset \in C (x) \leftrightarrow \emptyset \in C (0))$
9	8	notbid	$⊢ x = 0 \to (\neg \emptyset \in C (x) \leftrightarrow \neg \emptyset \in C (0))$
10	9	imbi2d	$⊢ x = 0 \to ((φ \to \neg \emptyset \in C (x)) \leftrightarrow (φ \to \neg \emptyset \in C (0)))$
11		fveq2	$⊢ x = k \to C (x) = C (k)$
12	11	eleq2d	$⊢ x = k \to (\emptyset \in C (x) \leftrightarrow \emptyset \in C (k))$
13	12	notbid	$⊢ x = k \to (\neg \emptyset \in C (x) \leftrightarrow \neg \emptyset \in C (k))$
14	13	imbi2d	$⊢ x = k \to ((φ \to \neg \emptyset \in C (x)) \leftrightarrow (φ \to \neg \emptyset \in C (k)))$
15		fveq2	$⊢ x = k + 1 \to C (x) = C (k + 1)$
16	15	eleq2d	$⊢ x = k + 1 \to (\emptyset \in C (x) \leftrightarrow \emptyset \in C (k + 1))$
17	16	notbid	$⊢ x = k + 1 \to (\neg \emptyset \in C (x) \leftrightarrow \neg \emptyset \in C (k + 1))$
18	17	imbi2d	$⊢ x = k + 1 \to ((φ \to \neg \emptyset \in C (x)) \leftrightarrow (φ \to \neg \emptyset \in C (k + 1)))$
19		fveq2	$⊢ x = N \to C (x) = C (N)$
20	19	eleq2d	$⊢ x = N \to (\emptyset \in C (x) \leftrightarrow \emptyset \in C (N))$
21	20	notbid	$⊢ x = N \to (\neg \emptyset \in C (x) \leftrightarrow \neg \emptyset \in C (N))$
22	21	imbi2d	$⊢ x = N \to ((φ \to \neg \emptyset \in C (x)) \leftrightarrow (φ \to \neg \emptyset \in C (N)))$
23	1 2 4	sadc0	$⊢ φ \to \neg \emptyset \in C (0)$
24		noel	$⊢ \neg k \in \emptyset$
25	1	ad2antrr	$⊢ ((φ \land k \in ℕ_{0}) \land \neg \emptyset \in C (k)) \to A \subseteq ℕ_{0}$
26	2	ad2antrr	$⊢ ((φ \land k \in ℕ_{0}) \land \neg \emptyset \in C (k)) \to B \subseteq ℕ_{0}$
27		simplr	$⊢ ((φ \land k \in ℕ_{0}) \land \neg \emptyset \in C (k)) \to k \in ℕ_{0}$
28	25 26 4 27	sadcp1	$⊢ ((φ \land k \in ℕ_{0}) \land \neg \emptyset \in C (k)) \to (\emptyset \in C (k + 1) \leftrightarrow cadd (k \in A, k \in B, \emptyset \in C (k)))$
29		cad0	$⊢ \neg \emptyset \in C (k) \to (cadd (k \in A, k \in B, \emptyset \in C (k)) \leftrightarrow (k \in A \land k \in B))$
30	29	adantl	$⊢ ((φ \land k \in ℕ_{0}) \land \neg \emptyset \in C (k)) \to (cadd (k \in A, k \in B, \emptyset \in C (k)) \leftrightarrow (k \in A \land k \in B))$
31		elin	$⊢ k \in (A \cap B) \leftrightarrow (k \in A \land k \in B)$
32	3	ad2antrr	$⊢ ((φ \land k \in ℕ_{0}) \land \neg \emptyset \in C (k)) \to A \cap B = \emptyset$
33	32	eleq2d	$⊢ ((φ \land k \in ℕ_{0}) \land \neg \emptyset \in C (k)) \to (k \in (A \cap B) \leftrightarrow k \in \emptyset)$
34	31 33	bitr3id	$⊢ ((φ \land k \in ℕ_{0}) \land \neg \emptyset \in C (k)) \to ((k \in A \land k \in B) \leftrightarrow k \in \emptyset)$
35	28 30 34	3bitrd	$⊢ ((φ \land k \in ℕ_{0}) \land \neg \emptyset \in C (k)) \to (\emptyset \in C (k + 1) \leftrightarrow k \in \emptyset)$
36	24 35	mtbiri	$⊢ ((φ \land k \in ℕ_{0}) \land \neg \emptyset \in C (k)) \to \neg \emptyset \in C (k + 1)$
37	36	ex	$⊢ (φ \land k \in ℕ_{0}) \to (\neg \emptyset \in C (k) \to \neg \emptyset \in C (k + 1))$
38	37	expcom	$⊢ k \in ℕ_{0} \to (φ \to (\neg \emptyset \in C (k) \to \neg \emptyset \in C (k + 1)))$
39	38	a2d	$⊢ k \in ℕ_{0} \to ((φ \to \neg \emptyset \in C (k)) \to (φ \to \neg \emptyset \in C (k + 1)))$
40	10 14 18 22 23 39	nn0ind	$⊢ N \in ℕ_{0} \to (φ \to \neg \emptyset \in C (N))$
41	5 40	mpcom	$⊢ φ \to \neg \emptyset \in C (N)$
42		hadrot	$⊢ hadd (\emptyset \in C (N), N \in A, N \in B) \leftrightarrow hadd (N \in A, N \in B, \emptyset \in C (N))$
43		had0	$⊢ \neg \emptyset \in C (N) \to (hadd (\emptyset \in C (N), N \in A, N \in B) \leftrightarrow (N \in A ⊻ N \in B))$
44	42 43	bitr3id	$⊢ \neg \emptyset \in C (N) \to (hadd (N \in A, N \in B, \emptyset \in C (N)) \leftrightarrow (N \in A ⊻ N \in B))$
45	41 44	syl	$⊢ φ \to (hadd (N \in A, N \in B, \emptyset \in C (N)) \leftrightarrow (N \in A ⊻ N \in B))$
46		noel	$⊢ \neg N \in \emptyset$
47		elin	$⊢ N \in (A \cap B) \leftrightarrow (N \in A \land N \in B)$
48	3	eleq2d	$⊢ φ \to (N \in (A \cap B) \leftrightarrow N \in \emptyset)$
49	47 48	bitr3id	$⊢ φ \to ((N \in A \land N \in B) \leftrightarrow N \in \emptyset)$
50	46 49	mtbiri	$⊢ φ \to \neg (N \in A \land N \in B)$
51		xor2	$⊢ (N \in A ⊻ N \in B) \leftrightarrow ((N \in A \lor N \in B) \land \neg (N \in A \land N \in B))$
52	51	rbaib	$⊢ \neg (N \in A \land N \in B) \to ((N \in A ⊻ N \in B) \leftrightarrow (N \in A \lor N \in B))$
53	50 52	syl	$⊢ φ \to ((N \in A ⊻ N \in B) \leftrightarrow (N \in A \lor N \in B))$
54		elun	$⊢ N \in (A \cup B) \leftrightarrow (N \in A \lor N \in B)$
55	53 54	bitr4di	$⊢ φ \to ((N \in A ⊻ N \in B) \leftrightarrow N \in (A \cup B))$
56	6 45 55	3bitrd	$⊢ φ \to (N \in (A sadd B) \leftrightarrow N \in (A \cup B))$

Metamath Proof Explorer

Theorem saddisjlem

Proof