Theorem iundisj2 25598

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

Hypothesis

Ref	Expression
iundisj.1	⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)

Assertion

Ref	Expression
iundisj2	⊢ Disj 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)

Distinct variable groups:   𝑘,𝑛   𝐴,𝑘   𝐵,𝑛

Allowed substitution hints:   𝐴(𝑛)   𝐵(𝑘)

Proof of Theorem iundisj2

Dummy variables 𝑎 𝑏 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tru 1541	. . . 4 ⊢ ⊤
2		eqeq12 2752	. . . . . 6 ⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (𝑎 = 𝑏 ↔ 𝑥 = 𝑦))
3		csbeq1 3911	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → ⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) = ⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵))
4		csbeq1 3911	. . . . . . . 8 ⊢ (𝑏 = 𝑦 → ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) = ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵))
5	3, 4	ineqan12d 4230	. . . . . . 7 ⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)))
6	5	eqeq1d 2737	. . . . . 6 ⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → ((⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅ ↔ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅))
7	2, 6	orbi12d 918	. . . . 5 ⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → ((𝑎 = 𝑏 ∨ (⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅) ↔ (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅)))
8		eqeq12 2752	. . . . . . 7 ⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (𝑎 = 𝑏 ↔ 𝑦 = 𝑥))
9		equcom 2015	. . . . . . 7 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦)
10	8, 9	bitrdi 287	. . . . . 6 ⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (𝑎 = 𝑏 ↔ 𝑥 = 𝑦))
11		csbeq1 3911	. . . . . . . . 9 ⊢ (𝑎 = 𝑦 → ⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) = ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵))
12		csbeq1 3911	. . . . . . . . 9 ⊢ (𝑏 = 𝑥 → ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) = ⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵))
13	11, 12	ineqan12d 4230	. . . . . . . 8 ⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = (⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)))
14		incom 4217	. . . . . . . 8 ⊢ (⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵))
15	13, 14	eqtrdi 2791	. . . . . . 7 ⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)))
16	15	eqeq1d 2737	. . . . . 6 ⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → ((⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅ ↔ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅))
17	10, 16	orbi12d 918	. . . . 5 ⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → ((𝑎 = 𝑏 ∨ (⦋𝑎 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑏 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅) ↔ (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅)))
18		nnssre 12268	. . . . . 6 ⊢ ℕ ⊆ ℝ
19	18	a1i 11	. . . . 5 ⊢ (⊤ → ℕ ⊆ ℝ)
20		biidd 262	. . . . 5 ⊢ ((⊤ ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ)) → ((𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅) ↔ (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅)))
21		nesym 2995	. . . . . . . 8 ⊢ (𝑦 ≠ 𝑥 ↔ ¬ 𝑥 = 𝑦)
22		nnre 12271	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℝ)
23		nnre 12271	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
24		id 22	. . . . . . . . . 10 ⊢ (𝑥 ≤ 𝑦 → 𝑥 ≤ 𝑦)
25		leltne 11348	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦) → (𝑥 < 𝑦 ↔ 𝑦 ≠ 𝑥))
26	22, 23, 24, 25	syl3an 1159	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦) → (𝑥 < 𝑦 ↔ 𝑦 ≠ 𝑥))
27		vex 3482	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
28		nfcsb1v 3933	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛⦋𝑥 / 𝑛⦌𝐴
29		nfcv 2903	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛∪ 𝑘 ∈ (1..^𝑥)𝐵
30	28, 29	nfdif 4139	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛(⦋𝑥 / 𝑛⦌𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑥)𝐵)
31		csbeq1a 3922	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑥 → 𝐴 = ⦋𝑥 / 𝑛⦌𝐴)
32		oveq2 7439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑥 → (1..^𝑛) = (1..^𝑥))
33	32	iuneq1d 5024	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑥 → ∪ 𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^𝑥)𝐵)
34	31, 33	difeq12d 4137	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑥 → (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑥 / 𝑛⦌𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑥)𝐵))
35	27, 30, 34	csbief 3943	. . . . . . . . . . . . . 14 ⊢ ⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑥 / 𝑛⦌𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑥)𝐵)
36		vex 3482	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
37		nfcsb1v 3933	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛⦋𝑦 / 𝑛⦌𝐴
38		nfcv 2903	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛∪ 𝑘 ∈ (1..^𝑦)𝐵
39	37, 38	nfdif 4139	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛(⦋𝑦 / 𝑛⦌𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑦)𝐵)
40		csbeq1a 3922	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑦 → 𝐴 = ⦋𝑦 / 𝑛⦌𝐴)
41		oveq2 7439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑦 → (1..^𝑛) = (1..^𝑦))
42	41	iuneq1d 5024	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑦 → ∪ 𝑘 ∈ (1..^𝑛)𝐵 = ∪ 𝑘 ∈ (1..^𝑦)𝐵)
43	40, 42	difeq12d 4137	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑦 → (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑦)𝐵))
44	36, 39, 43	csbief 3943	. . . . . . . . . . . . . 14 ⊢ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) = (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑦)𝐵)
45	35, 44	ineq12i 4226	. . . . . . . . . . . . 13 ⊢ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ((⦋𝑥 / 𝑛⦌𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑥)𝐵) ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑦)𝐵))
46		simp1 1135	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → 𝑥 ∈ ℕ)
47		nnuz 12919	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ = (ℤ≥‘1)
48	46, 47	eleqtrdi 2849	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → 𝑥 ∈ (ℤ≥‘1))
49		simp2 1136	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℕ)
50	49	nnzd 12638	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℤ)
51		simp3 1137	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → 𝑥 < 𝑦)
52		elfzo2 13699	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (1..^𝑦) ↔ (𝑥 ∈ (ℤ≥‘1) ∧ 𝑦 ∈ ℤ ∧ 𝑥 < 𝑦))
53	48, 50, 51, 52	syl3anbrc 1342	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → 𝑥 ∈ (1..^𝑦))
54		nfcv 2903	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑛𝑘
55		nfcv 2903	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑛𝐵
56		iundisj.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)
57	54, 55, 56	csbhypf 3937	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑘 → ⦋𝑥 / 𝑛⦌𝐴 = 𝐵)
58	57	equcoms 2017	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑥 → ⦋𝑥 / 𝑛⦌𝐴 = 𝐵)
59	58	eqcomd 2741	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑥 → 𝐵 = ⦋𝑥 / 𝑛⦌𝐴)
60	59	ssiun2s 5053	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1..^𝑦) → ⦋𝑥 / 𝑛⦌𝐴 ⊆ ∪ 𝑘 ∈ (1..^𝑦)𝐵)
61	53, 60	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → ⦋𝑥 / 𝑛⦌𝐴 ⊆ ∪ 𝑘 ∈ (1..^𝑦)𝐵)
62	61	ssdifssd 4157	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → (⦋𝑥 / 𝑛⦌𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑥)𝐵) ⊆ ∪ 𝑘 ∈ (1..^𝑦)𝐵)
63	62	ssrind 4252	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → ((⦋𝑥 / 𝑛⦌𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑥)𝐵) ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑦)𝐵)) ⊆ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑦)𝐵)))
64	45, 63	eqsstrid 4044	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) ⊆ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑦)𝐵)))
65		disjdif 4478	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑦)𝐵)) = ∅
66		sseq0 4409	. . . . . . . . . . . 12 ⊢ (((⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) ⊆ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑦)𝐵)) ∧ (∪ 𝑘 ∈ (1..^𝑦)𝐵 ∩ (⦋𝑦 / 𝑛⦌𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑦)𝐵)) = ∅) → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅)
67	64, 65, 66	sylancl 586	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅)
68	67	3expia 1120	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥 < 𝑦 → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅))
69	68	3adant3 1131	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦) → (𝑥 < 𝑦 → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅))
70	26, 69	sylbird 260	. . . . . . . 8 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦) → (𝑦 ≠ 𝑥 → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅))
71	21, 70	biimtrrid 243	. . . . . . 7 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦) → (¬ 𝑥 = 𝑦 → (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅))
72	71	orrd 863	. . . . . 6 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦) → (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅))
73	72	adantl 481	. . . . 5 ⊢ ((⊤ ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ∧ 𝑥 ≤ 𝑦)) → (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅))
74	7, 17, 19, 20, 73	wlogle 11794	. . . 4 ⊢ ((⊤ ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ)) → (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅))
75	1, 74	mpan 690	. . 3 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅))
76	75	rgen2 3197	. 2 ⊢ ∀𝑥 ∈ ℕ ∀𝑦 ∈ ℕ (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅)
77		disjors 5131	. 2 ⊢ (Disj 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ↔ ∀𝑥 ∈ ℕ ∀𝑦 ∈ ℕ (𝑥 = 𝑦 ∨ (⦋𝑥 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) ∩ ⦋𝑦 / 𝑛⦌(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) = ∅))
78	76, 77	mpbir 231	1 ⊢ Disj 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1537  ⊤wtru 1538   ∈ wcel 2106   ≠ wne 2938  ∀wral 3059  ⦋csb 3908   ∖ cdif 3960   ∩ cin 3962   ⊆ wss 3963  ∅c0 4339  ∪ ciun 4996  Disj wdisj 5115   class class class wbr 5148  ‘cfv 6563  (class class class)co 7431  ℝcr 11152  1c1 11154   < clt 11293   ≤ cle 11294  ℕcn 12264  ℤcz 12611  ℤ_≥cuz 12876  ..^cfzo 13691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-disj 5116  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-nn 12265  df-n0 12525  df-z 12612  df-uz 12877  df-fz 13545  df-fzo 13692

This theorem is referenced by:  iunmbl  25602  volsup  25605  sigapildsys  34143  carsgclctunlem3  34302  voliunnfl  37651