Step | Hyp | Ref
| Expression |
1 | | eliun 4460 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) ↔ ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛)) |
2 | 1 | biimpi 205 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛)) |
3 | 2 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛)) |
4 | | iundjiun.nph |
. . . . . . . . 9
⊢
Ⅎ𝑛𝜑 |
5 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑛𝑥 |
6 | | nfiu1 4486 |
. . . . . . . . . 10
⊢
Ⅎ𝑛∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) |
7 | 5, 6 | nfel 2763 |
. . . . . . . . 9
⊢
Ⅎ𝑛 𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) |
8 | | simp2 1055 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹‘𝑛)) → 𝑛 ∈ (𝑁...𝑚)) |
9 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) → 𝜑) |
10 | | elfzuz 12209 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ (ℤ≥‘𝑁)) |
11 | | iundjiun.z |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑍 =
(ℤ≥‘𝑁) |
12 | 11 | eqcomi 2619 |
. . . . . . . . . . . . . . . . 17
⊢
(ℤ≥‘𝑁) = 𝑍 |
13 | 10, 12 | syl6eleq 2698 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ 𝑍) |
14 | 13 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) → 𝑛 ∈ 𝑍) |
15 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) |
16 | | iundjiun.e |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐸:𝑍⟶𝑉) |
17 | 16 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ 𝑉) |
18 | | difexg 4735 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸‘𝑛) ∈ 𝑉 → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) |
20 | | iundjiun.f |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
21 | 20 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ 𝑍 ∧ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
22 | 15, 19, 21 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
23 | | difssd 3700 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ⊆ (𝐸‘𝑛)) |
24 | 22, 23 | eqsstrd 3602 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ⊆ (𝐸‘𝑛)) |
25 | 9, 14, 24 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) → (𝐹‘𝑛) ⊆ (𝐸‘𝑛)) |
26 | 25 | 3adant3 1074 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹‘𝑛)) → (𝐹‘𝑛) ⊆ (𝐸‘𝑛)) |
27 | | simp3 1056 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹‘𝑛)) → 𝑥 ∈ (𝐹‘𝑛)) |
28 | 26, 27 | sseldd 3569 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹‘𝑛)) → 𝑥 ∈ (𝐸‘𝑛)) |
29 | | rspe 2986 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐸‘𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸‘𝑛)) |
30 | 8, 28, 29 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹‘𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸‘𝑛)) |
31 | | eliun 4460 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ↔ ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸‘𝑛)) |
32 | 30, 31 | sylibr 223 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹‘𝑛)) → 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
33 | 32 | 3exp 1256 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ (𝑁...𝑚) → (𝑥 ∈ (𝐹‘𝑛) → 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)))) |
34 | 4, 7, 33 | rexlimd 3008 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛) → 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))) |
35 | 34 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)) → (∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛) → 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))) |
36 | 3, 35 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)) → 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
37 | 36 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
38 | | dfss3 3558 |
. . . . 5
⊢ (∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) ⊆ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ↔ ∀𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
39 | 37, 38 | sylibr 223 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) ⊆ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
40 | | fzssuz 12253 |
. . . . . . . . . . 11
⊢ (𝑁...𝑚) ⊆ (ℤ≥‘𝑁) |
41 | 40 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) → (𝑁...𝑚) ⊆ (ℤ≥‘𝑁)) |
42 | 31 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸‘𝑛)) |
43 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛 𝑥 ∈ (𝐸‘𝑖) |
44 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑖 → (𝐸‘𝑛) = (𝐸‘𝑖)) |
45 | 44 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑖 → (𝑥 ∈ (𝐸‘𝑛) ↔ 𝑥 ∈ (𝐸‘𝑖))) |
46 | 43, 45 | uzwo4 38246 |
. . . . . . . . . 10
⊢ (((𝑁...𝑚) ⊆ (ℤ≥‘𝑁) ∧ ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸‘𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) |
47 | 41, 42, 46 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) → ∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) |
48 | 47 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) |
49 | | simprl 790 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) → 𝑥 ∈ (𝐸‘𝑛)) |
50 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑖(𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) |
51 | | nfra1 2925 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑖∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)) |
52 | 50, 51 | nfan 1816 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑖((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) |
53 | | elfzoelz 12339 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ ℤ) |
54 | 53 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ ℝ) |
55 | 54 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ ℝ) |
56 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ ℤ) |
57 | 56 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ ℝ) |
58 | 57 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑛 ∈ ℝ) |
59 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 1 ∈ ℝ) |
60 | 58, 59 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑛 − 1) ∈ ℝ) |
61 | | elfzolem1 38478 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ≤ (𝑛 − 1)) |
62 | 61 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ≤ (𝑛 − 1)) |
63 | 58 | ltm1d 10835 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑛 − 1) < 𝑛) |
64 | 55, 60, 58, 62, 63 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 < 𝑛) |
65 | 64 | ad4ant24 1290 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 < 𝑛) |
66 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑛 ∈ (𝑁...𝑚) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) |
67 | | elfzel1 12212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑁 ∈ ℤ) |
68 | 67 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑁 ∈ ℤ) |
69 | | elfzel2 12211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑚 ∈ ℤ) |
70 | 69 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑚 ∈ ℤ) |
71 | 53 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ ℤ) |
72 | 68, 70, 71 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑖 ∈ ℤ)) |
73 | | elfzole1 12347 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑁 ≤ 𝑖) |
74 | 73 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑁 ≤ 𝑖) |
75 | 70 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑚 ∈ ℝ) |
76 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑛 ∈ (𝑁...𝑚) → 1 ∈ ℝ) |
77 | 57, 76 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑛 ∈ (𝑁...𝑚) → (𝑛 − 1) ∈ ℝ) |
78 | 69 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑚 ∈ ℝ) |
79 | 57 | ltm1d 10835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑛 ∈ (𝑁...𝑚) → (𝑛 − 1) < 𝑛) |
80 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑛 ≤ 𝑚) |
81 | 77, 57, 78, 79, 80 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 ∈ (𝑁...𝑚) → (𝑛 − 1) < 𝑚) |
82 | 81 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑛 − 1) < 𝑚) |
83 | 55, 60, 75, 62, 82 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 < 𝑚) |
84 | 55, 75, 83 | ltled 10064 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ≤ 𝑚) |
85 | 72, 74, 84 | jca32 556 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → ((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑁 ≤ 𝑖 ∧ 𝑖 ≤ 𝑚))) |
86 | | elfz2 12204 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 ∈ (𝑁...𝑚) ↔ ((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑁 ≤ 𝑖 ∧ 𝑖 ≤ 𝑚))) |
87 | 85, 86 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ (𝑁...𝑚)) |
88 | 87 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑛 ∈ (𝑁...𝑚) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ (𝑁...𝑚)) |
89 | | rspa 2914 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((∀𝑖 ∈
(𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)) ∧ 𝑖 ∈ (𝑁...𝑚)) → (𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) |
90 | 66, 88, 89 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ (𝑁...𝑚) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) |
91 | 90 | adantlll 750 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) |
92 | 65, 91 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → ¬ 𝑥 ∈ (𝐸‘𝑖)) |
93 | 92 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → (𝑖 ∈ (𝑁..^𝑛) → ¬ 𝑥 ∈ (𝐸‘𝑖))) |
94 | 52, 93 | ralrimi 2940 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → ∀𝑖 ∈ (𝑁..^𝑛) ¬ 𝑥 ∈ (𝐸‘𝑖)) |
95 | | ralnex 2975 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑖 ∈
(𝑁..^𝑛) ¬ 𝑥 ∈ (𝐸‘𝑖) ↔ ¬ ∃𝑖 ∈ (𝑁..^𝑛)𝑥 ∈ (𝐸‘𝑖)) |
96 | 94, 95 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → ¬ ∃𝑖 ∈ (𝑁..^𝑛)𝑥 ∈ (𝐸‘𝑖)) |
97 | | eliun 4460 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ↔ ∃𝑖 ∈ (𝑁..^𝑛)𝑥 ∈ (𝐸‘𝑖)) |
98 | 96, 97 | sylnibr 318 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → ¬ 𝑥 ∈ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) |
99 | 98 | adantrl 748 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) → ¬ 𝑥 ∈ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) |
100 | 49, 99 | eldifd 3551 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) → 𝑥 ∈ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
101 | 14, 22 | syldan 486 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
102 | 101 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) = (𝐹‘𝑛)) |
103 | 102 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) = (𝐹‘𝑛)) |
104 | 100, 103 | eleqtrd 2690 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) → 𝑥 ∈ (𝐹‘𝑛)) |
105 | 104 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) → ((𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → 𝑥 ∈ (𝐹‘𝑛))) |
106 | 105 | ex 449 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑛 ∈ (𝑁...𝑚) → ((𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → 𝑥 ∈ (𝐹‘𝑛)))) |
107 | 4, 106 | reximdai 2995 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛))) |
108 | 107 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) → (∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛))) |
109 | 48, 108 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛)) |
110 | 109, 1 | sylibr 223 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) → 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)) |
111 | 110 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)) |
112 | | dfss3 3558 |
. . . . 5
⊢ (∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ⊆ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) ↔ ∀𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)) |
113 | 111, 112 | sylibr 223 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ⊆ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)) |
114 | 39, 113 | eqssd 3585 |
. . 3
⊢ (𝜑 → ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
115 | 114 | ralrimivw 2950 |
. 2
⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
116 | 11 | iuneqfzuz 38492 |
. . 3
⊢
(∀𝑚 ∈
𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) → ∪
𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
117 | 115, 116 | syl 17 |
. 2
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
118 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → (𝐸‘𝑛) = (𝐸‘𝑚)) |
119 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝑁..^𝑛) = (𝑁..^𝑚)) |
120 | 119 | iuneq1d 4481 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑁..^𝑚)(𝐸‘𝑖)) |
121 | 118, 120 | difeq12d 3691 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) = ((𝐸‘𝑚) ∖ ∪
𝑖 ∈ (𝑁..^𝑚)(𝐸‘𝑖))) |
122 | 121 | cbvmptv 4678 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) = (𝑚 ∈ 𝑍 ↦ ((𝐸‘𝑚) ∖ ∪
𝑖 ∈ (𝑁..^𝑚)(𝐸‘𝑖))) |
123 | 20, 122 | eqtri 2632 |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑚 ∈ 𝑍 ↦ ((𝐸‘𝑚) ∖ ∪
𝑖 ∈ (𝑁..^𝑚)(𝐸‘𝑖))) |
124 | | simpllr 795 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 < 𝑘) → 𝑛 ∈ 𝑍) |
125 | | simplr 788 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 < 𝑘) → 𝑘 ∈ 𝑍) |
126 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 < 𝑘) → 𝑛 < 𝑘) |
127 | 11, 123, 124, 125, 126 | iundjiunlem 39352 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 < 𝑘) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
128 | 127 | adantlr 747 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ 𝑛 < 𝑘) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
129 | | simpll 786 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → ((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍)) |
130 | | neqne 2790 |
. . . . . . . . . . . 12
⊢ (¬
𝑛 = 𝑘 → 𝑛 ≠ 𝑘) |
131 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ 𝑍) |
132 | 131, 11 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ (ℤ≥‘𝑁)) |
133 | | eluzelz 11573 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → 𝑘 ∈ ℤ) |
134 | 132, 133 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ) |
135 | 134 | zred 11358 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℝ) |
136 | 135 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℝ) |
137 | 136 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ ((((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 ≠ 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 ∈ ℝ) |
138 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍) |
139 | 138, 11 | syl6eleq 2698 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ≥‘𝑁)) |
140 | | eluzelz 11573 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘𝑁) → 𝑛 ∈ ℤ) |
141 | 139, 140 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ) |
142 | 141 | zred 11358 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℝ) |
143 | 142 | ad3antrrr 762 |
. . . . . . . . . . . . 13
⊢ ((((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 ≠ 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑛 ∈ ℝ) |
144 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 < 𝑘) → ¬ 𝑛 < 𝑘) |
145 | 136 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 < 𝑘) → 𝑘 ∈ ℝ) |
146 | 142 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 < 𝑘) → 𝑛 ∈ ℝ) |
147 | 145, 146 | lenltd 10062 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 < 𝑘) → (𝑘 ≤ 𝑛 ↔ ¬ 𝑛 < 𝑘)) |
148 | 144, 147 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 < 𝑘) → 𝑘 ≤ 𝑛) |
149 | 148 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ ((((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 ≠ 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 ≤ 𝑛) |
150 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ ((((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 ≠ 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑛 ≠ 𝑘) |
151 | 137, 143,
149, 150 | leneltd 10070 |
. . . . . . . . . . . 12
⊢ ((((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 ≠ 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 < 𝑛) |
152 | 130, 151 | sylanl2 681 |
. . . . . . . . . . 11
⊢ ((((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 < 𝑛) |
153 | 152 | ad5ant2345 1309 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 < 𝑛) |
154 | | anass 679 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ↔ (𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍))) |
155 | | incom 3767 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ((𝐹‘𝑘) ∩ (𝐹‘𝑛)) |
156 | 155 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍)) ∧ 𝑘 < 𝑛) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ((𝐹‘𝑘) ∩ (𝐹‘𝑛))) |
157 | | simplrr 797 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍)) ∧ 𝑘 < 𝑛) → 𝑘 ∈ 𝑍) |
158 | | simplrl 796 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍)) ∧ 𝑘 < 𝑛) → 𝑛 ∈ 𝑍) |
159 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍)) ∧ 𝑘 < 𝑛) → 𝑘 < 𝑛) |
160 | 11, 123, 157, 158, 159 | iundjiunlem 39352 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍)) ∧ 𝑘 < 𝑛) → ((𝐹‘𝑘) ∩ (𝐹‘𝑛)) = ∅) |
161 | 156, 160 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍)) ∧ 𝑘 < 𝑛) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
162 | 154, 161 | sylanb 488 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ 𝑘 < 𝑛) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
163 | 129, 153,
162 | syl2anc 691 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
164 | 128, 163 | pm2.61dan 828 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 = 𝑘) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
165 | 164 | ex 449 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (¬ 𝑛 = 𝑘 → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
166 | | df-or 384 |
. . . . . . 7
⊢ ((𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) ↔ (¬ 𝑛 = 𝑘 → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
167 | 165, 166 | sylibr 223 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
168 | 167 | ralrimiva 2949 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
169 | 168 | ex 449 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ 𝑍 → ∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅))) |
170 | 4, 169 | ralrimi 2940 |
. . 3
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 ∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
171 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑚(𝐹‘𝑛) |
172 | | nfmpt1 4675 |
. . . . . . 7
⊢
Ⅎ𝑛(𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
173 | 20, 172 | nfcxfr 2749 |
. . . . . 6
⊢
Ⅎ𝑛𝐹 |
174 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑛𝑚 |
175 | 173, 174 | nffv 6110 |
. . . . 5
⊢
Ⅎ𝑛(𝐹‘𝑚) |
176 | | fveq2 6103 |
. . . . 5
⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚)) |
177 | 171, 175,
176 | cbvdisj 4563 |
. . . 4
⊢
(Disj 𝑛
∈ 𝑍 (𝐹‘𝑛) ↔ Disj 𝑚 ∈ 𝑍 (𝐹‘𝑚)) |
178 | | fveq2 6103 |
. . . . 5
⊢ (𝑚 = 𝑘 → (𝐹‘𝑚) = (𝐹‘𝑘)) |
179 | 178 | disjor 4567 |
. . . 4
⊢
(Disj 𝑚
∈ 𝑍 (𝐹‘𝑚) ↔ ∀𝑚 ∈ 𝑍 ∀𝑘 ∈ 𝑍 (𝑚 = 𝑘 ∨ ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅)) |
180 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑛𝑍 |
181 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑛 𝑚 = 𝑘 |
182 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑛𝑘 |
183 | 173, 182 | nffv 6110 |
. . . . . . . . 9
⊢
Ⅎ𝑛(𝐹‘𝑘) |
184 | 175, 183 | nfin 3782 |
. . . . . . . 8
⊢
Ⅎ𝑛((𝐹‘𝑚) ∩ (𝐹‘𝑘)) |
185 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑛∅ |
186 | 184, 185 | nfeq 2762 |
. . . . . . 7
⊢
Ⅎ𝑛((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅ |
187 | 181, 186 | nfor 1822 |
. . . . . 6
⊢
Ⅎ𝑛(𝑚 = 𝑘 ∨ ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅) |
188 | 180, 187 | nfral 2929 |
. . . . 5
⊢
Ⅎ𝑛∀𝑘 ∈ 𝑍 (𝑚 = 𝑘 ∨ ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅) |
189 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑚∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
190 | | equequ1 1939 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (𝑚 = 𝑘 ↔ 𝑛 = 𝑘)) |
191 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
192 | 191 | ineq1d 3775 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ((𝐹‘𝑛) ∩ (𝐹‘𝑘))) |
193 | 192 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅ ↔ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
194 | 190, 193 | orbi12d 742 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((𝑚 = 𝑘 ∨ ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅) ↔ (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅))) |
195 | 194 | ralbidv 2969 |
. . . . 5
⊢ (𝑚 = 𝑛 → (∀𝑘 ∈ 𝑍 (𝑚 = 𝑘 ∨ ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅) ↔ ∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅))) |
196 | 188, 189,
195 | cbvral 3143 |
. . . 4
⊢
(∀𝑚 ∈
𝑍 ∀𝑘 ∈ 𝑍 (𝑚 = 𝑘 ∨ ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅) ↔ ∀𝑛 ∈ 𝑍 ∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
197 | 177, 179,
196 | 3bitri 285 |
. . 3
⊢
(Disj 𝑛
∈ 𝑍 (𝐹‘𝑛) ↔ ∀𝑛 ∈ 𝑍 ∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
198 | 170, 197 | sylibr 223 |
. 2
⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛)) |
199 | 115, 117,
198 | jca31 555 |
1
⊢ (𝜑 → ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ ∪
𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∧ Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛))) |