iundisj2

Description: A disjoint union is disjoint. (Contributed by Mario Carneiro, 4-Jul-2014) (Revised by Mario Carneiro, 11-Dec-2016)

		Ref	Expression
	Hypothesis	iundisj.1	$⊢ n = k \to A = B$
	Assertion	iundisj2	$⊢ \underset{n \in ℕ}{Disj} (A ∖ ⋃_{k \in (1 ..^n)} B)$

Proof

Step	Hyp	Ref	Expression
1		iundisj.1	$⊢ n = k \to A = B$
2		tru	$⊢ ⊤$
3		eqeq12	$⊢ (a = x \land b = y) \to (a = b \leftrightarrow x = y)$
4		csbeq1	$⊢ a = x \to ⦋ a / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B)$
5		csbeq1	$⊢ b = y \to ⦋ b / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B)$
6	4 5	ineqan12d	$⊢ (a = x \land b = y) \to ⦋ a / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ b / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B)$
7	6	eqeq1d	$⊢ (a = x \land b = y) \to (⦋ a / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ b / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset \leftrightarrow ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset)$
8	3 7	orbi12d	$⊢ (a = x \land b = y) \to ((a = b \lor ⦋ a / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ b / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset) \leftrightarrow (x = y \lor ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset))$
9		eqeq12	$⊢ (a = y \land b = x) \to (a = b \leftrightarrow y = x)$
10		equcom	$⊢ y = x \leftrightarrow x = y$
11	9 10	bitrdi	$⊢ (a = y \land b = x) \to (a = b \leftrightarrow x = y)$
12		csbeq1	$⊢ a = y \to ⦋ a / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B)$
13		csbeq1	$⊢ b = x \to ⦋ b / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B)$
14	12 13	ineqan12d	$⊢ (a = y \land b = x) \to ⦋ a / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ b / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B)$
15		incom	$⊢ ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B)$
16	14 15	eqtrdi	$⊢ (a = y \land b = x) \to ⦋ a / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ b / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B)$
17	16	eqeq1d	$⊢ (a = y \land b = x) \to (⦋ a / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ b / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset \leftrightarrow ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset)$
18	11 17	orbi12d	$⊢ (a = y \land b = x) \to ((a = b \lor ⦋ a / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ b / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset) \leftrightarrow (x = y \lor ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset))$
19		nnssre	$⊢ ℕ \subseteq ℝ$
20	19	a1i	$⊢ ⊤ \to ℕ \subseteq ℝ$
21		biidd	$⊢ (⊤ \land (x \in ℕ \land y \in ℕ)) \to ((x = y \lor ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset) \leftrightarrow (x = y \lor ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset))$
22		nesym	$⊢ y \neq x \leftrightarrow \neg x = y$
23		nnre	$⊢ x \in ℕ \to x \in ℝ$
24		nnre	$⊢ y \in ℕ \to y \in ℝ$
25		id	$⊢ x \leq y \to x \leq y$
26		leltne	$⊢ (x \in ℝ \land y \in ℝ \land x \leq y) \to (x < y \leftrightarrow y \neq x)$
27	23 24 25 26	syl3an	$⊢ (x \in ℕ \land y \in ℕ \land x \leq y) \to (x < y \leftrightarrow y \neq x)$
28		vex	$⊢ x \in V$
29		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ x / n ⦌ A$
30		nfcv	$⊢ \underline{Ⅎ} n ⋃_{k \in (1 ..^x)} B$
31	29 30	nfdif	$⊢ \underline{Ⅎ} n (⦋ x / n ⦌ A ∖ ⋃_{k \in (1 ..^x)} B)$
32		csbeq1a	$⊢ n = x \to A = ⦋ x / n ⦌ A$
33		oveq2	$⊢ n = x \to (1 ..^n) = (1 ..^x)$
34	33	iuneq1d	$⊢ n = x \to ⋃_{k \in (1 ..^n)} B = ⋃_{k \in (1 ..^x)} B$
35	32 34	difeq12d	$⊢ n = x \to A ∖ ⋃_{k \in (1 ..^n)} B = ⦋ x / n ⦌ A ∖ ⋃_{k \in (1 ..^x)} B$
36	28 31 35	csbief	$⊢ ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = ⦋ x / n ⦌ A ∖ ⋃_{k \in (1 ..^x)} B$
37		vex	$⊢ y \in V$
38		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ y / n ⦌ A$
39		nfcv	$⊢ \underline{Ⅎ} n ⋃_{k \in (1 ..^y)} B$
40	38 39	nfdif	$⊢ \underline{Ⅎ} n (⦋ y / n ⦌ A ∖ ⋃_{k \in (1 ..^y)} B)$
41		csbeq1a	$⊢ n = y \to A = ⦋ y / n ⦌ A$
42		oveq2	$⊢ n = y \to (1 ..^n) = (1 ..^y)$
43	42	iuneq1d	$⊢ n = y \to ⋃_{k \in (1 ..^n)} B = ⋃_{k \in (1 ..^y)} B$
44	41 43	difeq12d	$⊢ n = y \to A ∖ ⋃_{k \in (1 ..^n)} B = ⦋ y / n ⦌ A ∖ ⋃_{k \in (1 ..^y)} B$
45	37 40 44	csbief	$⊢ ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = ⦋ y / n ⦌ A ∖ ⋃_{k \in (1 ..^y)} B$
46	36 45	ineq12i	$⊢ ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = (⦋ x / n ⦌ A ∖ ⋃_{k \in (1 ..^x)} B) \cap (⦋ y / n ⦌ A ∖ ⋃_{k \in (1 ..^y)} B)$
47		simp1	$⊢ (x \in ℕ \land y \in ℕ \land x < y) \to x \in ℕ$
48		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
49	47 48	eleqtrdi	$⊢ (x \in ℕ \land y \in ℕ \land x < y) \to x \in ℤ_{\geq 1}$
50		simp2	$⊢ (x \in ℕ \land y \in ℕ \land x < y) \to y \in ℕ$
51	50	nnzd	$⊢ (x \in ℕ \land y \in ℕ \land x < y) \to y \in ℤ$
52		simp3	$⊢ (x \in ℕ \land y \in ℕ \land x < y) \to x < y$
53		elfzo2	$⊢ x \in (1 ..^y) \leftrightarrow (x \in ℤ_{\geq 1} \land y \in ℤ \land x < y)$
54	49 51 52 53	syl3anbrc	$⊢ (x \in ℕ \land y \in ℕ \land x < y) \to x \in (1 ..^y)$
55		nfcv	$⊢ \underline{Ⅎ} n k$
56		nfcv	$⊢ \underline{Ⅎ} n B$
57	55 56 1	csbhypf	$⊢ x = k \to ⦋ x / n ⦌ A = B$
58	57	equcoms	$⊢ k = x \to ⦋ x / n ⦌ A = B$
59	58	eqcomd	$⊢ k = x \to B = ⦋ x / n ⦌ A$
60	59	ssiun2s	$⊢ x \in (1 ..^y) \to ⦋ x / n ⦌ A \subseteq ⋃_{k \in (1 ..^y)} B$
61	54 60	syl	$⊢ (x \in ℕ \land y \in ℕ \land x < y) \to ⦋ x / n ⦌ A \subseteq ⋃_{k \in (1 ..^y)} B$
62	61	ssdifssd	$⊢ (x \in ℕ \land y \in ℕ \land x < y) \to ⦋ x / n ⦌ A ∖ ⋃_{k \in (1 ..^x)} B \subseteq ⋃_{k \in (1 ..^y)} B$
63	62	ssrind	$⊢ (x \in ℕ \land y \in ℕ \land x < y) \to (⦋ x / n ⦌ A ∖ ⋃_{k \in (1 ..^x)} B) \cap (⦋ y / n ⦌ A ∖ ⋃_{k \in (1 ..^y)} B) \subseteq ⋃_{k \in (1 ..^y)} B \cap (⦋ y / n ⦌ A ∖ ⋃_{k \in (1 ..^y)} B)$
64	46 63	eqsstrid	$⊢ (x \in ℕ \land y \in ℕ \land x < y) \to ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \subseteq ⋃_{k \in (1 ..^y)} B \cap (⦋ y / n ⦌ A ∖ ⋃_{k \in (1 ..^y)} B)$
65		disjdif	$⊢ ⋃_{k \in (1 ..^y)} B \cap (⦋ y / n ⦌ A ∖ ⋃_{k \in (1 ..^y)} B) = \emptyset$
66		sseq0	$⊢ (⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \subseteq ⋃_{k \in (1 ..^y)} B \cap (⦋ y / n ⦌ A ∖ ⋃_{k \in (1 ..^y)} B) \land ⋃_{k \in (1 ..^y)} B \cap (⦋ y / n ⦌ A ∖ ⋃_{k \in (1 ..^y)} B) = \emptyset) \to ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset$
67	64 65 66	sylancl	$⊢ (x \in ℕ \land y \in ℕ \land x < y) \to ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset$
68	67	3expia	$⊢ (x \in ℕ \land y \in ℕ) \to (x < y \to ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset)$
69	68	3adant3	$⊢ (x \in ℕ \land y \in ℕ \land x \leq y) \to (x < y \to ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset)$
70	27 69	sylbird	$⊢ (x \in ℕ \land y \in ℕ \land x \leq y) \to (y \neq x \to ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset)$
71	22 70	biimtrrid	$⊢ (x \in ℕ \land y \in ℕ \land x \leq y) \to (\neg x = y \to ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset)$
72	71	orrd	$⊢ (x \in ℕ \land y \in ℕ \land x \leq y) \to (x = y \lor ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset)$
73	72	adantl	$⊢ (⊤ \land (x \in ℕ \land y \in ℕ \land x \leq y)) \to (x = y \lor ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset)$
74	8 18 20 21 73	wlogle	$⊢ (⊤ \land (x \in ℕ \land y \in ℕ)) \to (x = y \lor ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset)$
75	2 74	mpan	$⊢ (x \in ℕ \land y \in ℕ) \to (x = y \lor ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset)$
76	75	rgen2	$⊢ \forall x \in ℕ \forall y \in ℕ (x = y \lor ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset)$
77		disjors	$⊢ \underset{n \in ℕ}{Disj} (A ∖ ⋃_{k \in (1 ..^n)} B) \leftrightarrow \forall x \in ℕ \forall y \in ℕ (x = y \lor ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) \cap ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = \emptyset)$
78	76 77	mpbir	$⊢ \underset{n \in ℕ}{Disj} (A ∖ ⋃_{k \in (1 ..^n)} B)$

Metamath Proof Explorer

Theorem iundisj2

Proof