iundisj2fi

Description: A disjoint union is disjoint, finite version. Cf. iundisj2 . (Contributed by Thierry Arnoux, 16-Feb-2017)

	Ref	Expression
Hypotheses	iundisj2fi.0	$⊢ \underline{Ⅎ} n B$
	iundisj2fi.1	$⊢ n = k \to A = B$
Assertion	iundisj2fi	$⊢ \underset{n \in (1 ..^N)}{Disj} (A ∖ ⋃_{k \in (1 ..^n)} B)$

Proof

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

Metamath Proof Explorer

Theorem iundisj2fi

Proof