iundisj2f

Description: A disjoint union is disjoint. Cf. iundisj2 . (Contributed by Thierry Arnoux, 30-Dec-2016)

	Ref	Expression
Hypotheses	iundisjf.1	$⊢ \underline{Ⅎ} k A$
	iundisjf.2	$⊢ \underline{Ⅎ} n B$
	iundisjf.3	$⊢ n = k \to A = B$
Assertion	iundisj2f	$⊢ \underset{n \in ℕ}{Disj} (A ∖ ⋃_{k \in (1 ..^n)} B)$

Proof

Step	Hyp	Ref	Expression
1		iundisjf.1	$⊢ \underline{Ⅎ} k A$
2		iundisjf.2	$⊢ \underline{Ⅎ} n B$
3		iundisjf.3	$⊢ n = k \to A = B$
4		tru	$⊢ ⊤$
5		eqeq12	$⊢ (a = x \land b = y) \to (a = b \leftrightarrow x = y)$
6		csbeq1	$⊢ a = x \to ⦋ a / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B)$
7		csbeq1	$⊢ b = y \to ⦋ b / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B)$
8	6 7	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)$
9	8	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)$
10	5 9	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))$
11		eqeq12	$⊢ (a = y \land b = x) \to (a = b \leftrightarrow y = x)$
12		equcom	$⊢ y = x \leftrightarrow x = y$
13	11 12	bitrdi	$⊢ (a = y \land b = x) \to (a = b \leftrightarrow x = y)$
14		csbeq1	$⊢ a = y \to ⦋ a / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B)$
15		csbeq1	$⊢ b = x \to ⦋ b / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B)$
16	14 15	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)$
17		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)$
18	16 17	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)$
19	18	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)$
20	13 19	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))$
21		nnssre	$⊢ ℕ \subseteq ℝ$
22	21	a1i	$⊢ ⊤ \to ℕ \subseteq ℝ$
23		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))$
24		nesym	$⊢ y \neq x \leftrightarrow \neg x = y$
25		nnre	$⊢ x \in ℕ \to x \in ℝ$
26		nnre	$⊢ y \in ℕ \to y \in ℝ$
27		id	$⊢ x \leq y \to x \leq y$
28		leltne	$⊢ (x \in ℝ \land y \in ℝ \land x \leq y) \to (x < y \leftrightarrow y \neq x)$
29	25 26 27 28	syl3an	$⊢ (x \in ℕ \land y \in ℕ \land x \leq y) \to (x < y \leftrightarrow y \neq x)$
30		vex	$⊢ x \in V$
31		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ x / n ⦌ A$
32		nfcv	$⊢ \underline{Ⅎ} n (1 ..^x)$
33	32 2	nfiun	$⊢ \underline{Ⅎ} n ⋃_{k \in (1 ..^x)} B$
34	31 33	nfdif	$⊢ \underline{Ⅎ} n (⦋ x / n ⦌ A ∖ ⋃_{k \in (1 ..^x)} B)$
35		csbeq1a	$⊢ n = x \to A = ⦋ x / n ⦌ A$
36		oveq2	$⊢ n = x \to (1 ..^n) = (1 ..^x)$
37	36	iuneq1d	$⊢ n = x \to ⋃_{k \in (1 ..^n)} B = ⋃_{k \in (1 ..^x)} B$
38	35 37	difeq12d	$⊢ n = x \to A ∖ ⋃_{k \in (1 ..^n)} B = ⦋ x / n ⦌ A ∖ ⋃_{k \in (1 ..^x)} B$
39	30 34 38	csbief	$⊢ ⦋ x / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = ⦋ x / n ⦌ A ∖ ⋃_{k \in (1 ..^x)} B$
40		vex	$⊢ y \in V$
41		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ y / n ⦌ A$
42		nfcv	$⊢ \underline{Ⅎ} n (1 ..^y)$
43	42 2	nfiun	$⊢ \underline{Ⅎ} n ⋃_{k \in (1 ..^y)} B$
44	41 43	nfdif	$⊢ \underline{Ⅎ} n (⦋ y / n ⦌ A ∖ ⋃_{k \in (1 ..^y)} B)$
45		csbeq1a	$⊢ n = y \to A = ⦋ y / n ⦌ A$
46		oveq2	$⊢ n = y \to (1 ..^n) = (1 ..^y)$
47	46	iuneq1d	$⊢ n = y \to ⋃_{k \in (1 ..^n)} B = ⋃_{k \in (1 ..^y)} B$
48	45 47	difeq12d	$⊢ n = y \to A ∖ ⋃_{k \in (1 ..^n)} B = ⦋ y / n ⦌ A ∖ ⋃_{k \in (1 ..^y)} B$
49	40 44 48	csbief	$⊢ ⦋ y / n ⦌ (A ∖ ⋃_{k \in (1 ..^n)} B) = ⦋ y / n ⦌ A ∖ ⋃_{k \in (1 ..^y)} B$
50	39 49	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)$
51		simp1	$⊢ (x \in ℕ \land y \in ℕ \land x < y) \to x \in ℕ$
52		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
53	51 52	eleqtrdi	$⊢ (x \in ℕ \land y \in ℕ \land x < y) \to x \in ℤ_{\geq 1}$
54		simp2	$⊢ (x \in ℕ \land y \in ℕ \land x < y) \to y \in ℕ$
55	54	nnzd	$⊢ (x \in ℕ \land y \in ℕ \land x < y) \to y \in ℤ$
56		simp3	$⊢ (x \in ℕ \land y \in ℕ \land x < y) \to x < y$
57		elfzo2	$⊢ x \in (1 ..^y) \leftrightarrow (x \in ℤ_{\geq 1} \land y \in ℤ \land x < y)$
58	53 55 56 57	syl3anbrc	$⊢ (x \in ℕ \land y \in ℕ \land x < y) \to x \in (1 ..^y)$
59		nfcv	$⊢ \underline{Ⅎ} k (1 ..^y)$
60		nfcv	$⊢ \underline{Ⅎ} k x$
61	60 1	nfcsbw	$⊢ \underline{Ⅎ} k ⦋ x / n ⦌ A$
62		nfcv	$⊢ \underline{Ⅎ} n k$
63	62 2 3	csbhypf	$⊢ x = k \to ⦋ x / n ⦌ A = B$
64	63	equcoms	$⊢ k = x \to ⦋ x / n ⦌ A = B$
65	64	eqcomd	$⊢ k = x \to B = ⦋ x / n ⦌ A$
66	59 60 61 65	ssiun2sf	$⊢ x \in (1 ..^y) \to ⦋ x / n ⦌ A \subseteq ⋃_{k \in (1 ..^y)} B$
67	58 66	syl	$⊢ (x \in ℕ \land y \in ℕ \land x < y) \to ⦋ x / n ⦌ A \subseteq ⋃_{k \in (1 ..^y)} B$
68	67	ssdifssd	$⊢ (x \in ℕ \land y \in ℕ \land x < y) \to ⦋ x / n ⦌ A ∖ ⋃_{k \in (1 ..^x)} B \subseteq ⋃_{k \in (1 ..^y)} B$
69	68	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)$
70	50 69	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)$
71		disjdif	$⊢ ⋃_{k \in (1 ..^y)} B \cap (⦋ y / n ⦌ A ∖ ⋃_{k \in (1 ..^y)} B) = \emptyset$
72		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$
73	70 71 72	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$
74	73	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)$
75	74	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)$
76	29 75	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)$
77	24 76	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)$
78	77	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)$
79	78	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)$
80	10 20 22 23 79	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)$
81	4 80	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)$
82	81	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)$
83		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)$
84	82 83	mpbir	$⊢ \underset{n \in ℕ}{Disj} (A ∖ ⋃_{k \in (1 ..^n)} B)$

Metamath Proof Explorer

Theorem iundisj2f

Proof