Step | Hyp | Ref
| Expression |
1 | | eliun 4916 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) ↔ ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛)) |
2 | 1 | biimpi 217 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛)) |
3 | 2 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛)) |
4 | | iundjiun.nph |
. . . . . . . . 9
⊢
Ⅎ𝑛𝜑 |
5 | | nfcv 2977 |
. . . . . . . . . 10
⊢
Ⅎ𝑛𝑥 |
6 | | nfiu1 4945 |
. . . . . . . . . 10
⊢
Ⅎ𝑛∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) |
7 | 5, 6 | nfel 2992 |
. . . . . . . . 9
⊢
Ⅎ𝑛 𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) |
8 | | simp2 1129 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹‘𝑛)) → 𝑛 ∈ (𝑁...𝑚)) |
9 | | simpl 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) → 𝜑) |
10 | | elfzuz 12894 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ (ℤ≥‘𝑁)) |
11 | | iundjiun.z |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑍 =
(ℤ≥‘𝑁) |
12 | 11 | eqcomi 2830 |
. . . . . . . . . . . . . . . . 17
⊢
(ℤ≥‘𝑁) = 𝑍 |
13 | 10, 12 | eleqtrdi 2923 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ 𝑍) |
14 | 13 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) → 𝑛 ∈ 𝑍) |
15 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) |
16 | | iundjiun.e |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐸:𝑍⟶𝑉) |
17 | 16 | ffvelrnda 6844 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ 𝑉) |
18 | | difexg 5223 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸‘𝑛) ∈ 𝑉 → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) |
20 | | iundjiun.f |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
21 | 20 | fvmpt2 6772 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ 𝑍 ∧ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
22 | 15, 19, 21 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
23 | | difssd 4108 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ⊆ (𝐸‘𝑛)) |
24 | 22, 23 | eqsstrd 4004 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ⊆ (𝐸‘𝑛)) |
25 | 9, 14, 24 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) → (𝐹‘𝑛) ⊆ (𝐸‘𝑛)) |
26 | 25 | 3adant3 1124 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹‘𝑛)) → (𝐹‘𝑛) ⊆ (𝐸‘𝑛)) |
27 | | simp3 1130 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹‘𝑛)) → 𝑥 ∈ (𝐹‘𝑛)) |
28 | 26, 27 | sseldd 3967 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹‘𝑛)) → 𝑥 ∈ (𝐸‘𝑛)) |
29 | | rspe 3304 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐸‘𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸‘𝑛)) |
30 | 8, 28, 29 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹‘𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸‘𝑛)) |
31 | | eliun 4916 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ↔ ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸‘𝑛)) |
32 | 30, 31 | sylibr 235 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹‘𝑛)) → 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
33 | 32 | 3exp 1111 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ (𝑁...𝑚) → (𝑥 ∈ (𝐹‘𝑛) → 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)))) |
34 | 4, 7, 33 | rexlimd 3317 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛) → 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))) |
35 | 34 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)) → (∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛) → 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))) |
36 | 3, 35 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)) → 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
37 | 36 | ralrimiva 3182 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
38 | | dfss3 3955 |
. . . . 5
⊢ (∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) ⊆ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ↔ ∀𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
39 | 37, 38 | sylibr 235 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) ⊆ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
40 | | fzssuz 12938 |
. . . . . . . . 9
⊢ (𝑁...𝑚) ⊆ (ℤ≥‘𝑁) |
41 | 40 | a1i 11 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) → (𝑁...𝑚) ⊆ (ℤ≥‘𝑁)) |
42 | 31 | biimpi 217 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸‘𝑛)) |
43 | | nfv 1906 |
. . . . . . . . 9
⊢
Ⅎ𝑛 𝑥 ∈ (𝐸‘𝑖) |
44 | | fveq2 6664 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑖 → (𝐸‘𝑛) = (𝐸‘𝑖)) |
45 | 44 | eleq2d 2898 |
. . . . . . . . 9
⊢ (𝑛 = 𝑖 → (𝑥 ∈ (𝐸‘𝑛) ↔ 𝑥 ∈ (𝐸‘𝑖))) |
46 | 43, 45 | uzwo4 41195 |
. . . . . . . 8
⊢ (((𝑁...𝑚) ⊆ (ℤ≥‘𝑁) ∧ ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸‘𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) |
47 | 41, 42, 46 | syl2anc 584 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) → ∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) |
48 | 47 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) |
49 | | simprl 767 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) → 𝑥 ∈ (𝐸‘𝑛)) |
50 | | nfv 1906 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑖(𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) |
51 | | nfra1 3219 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑖∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)) |
52 | 50, 51 | nfan 1891 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑖((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) |
53 | | elfzoelz 13028 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ ℤ) |
54 | 53 | zred 12076 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ ℝ) |
55 | 54 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ ℝ) |
56 | | elfzelz 12898 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ ℤ) |
57 | 56 | zred 12076 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ ℝ) |
58 | 57 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑛 ∈ ℝ) |
59 | | 1red 10631 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 1 ∈ ℝ) |
60 | 58, 59 | resubcld 11057 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑛 − 1) ∈ ℝ) |
61 | | elfzolem1 41469 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ≤ (𝑛 − 1)) |
62 | 61 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ≤ (𝑛 − 1)) |
63 | 58 | ltm1d 11561 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑛 − 1) < 𝑛) |
64 | 55, 60, 58, 62, 63 | lelttrd 10787 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 < 𝑛) |
65 | 64 | ad4ant24 750 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 < 𝑛) |
66 | | simplr 765 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ (𝑁...𝑚) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) |
67 | | elfzel1 12897 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑁 ∈ ℤ) |
68 | 67 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑁 ∈ ℤ) |
69 | | elfzel2 12896 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑚 ∈ ℤ) |
70 | 69 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑚 ∈ ℤ) |
71 | 53 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ ℤ) |
72 | 68, 70, 71 | 3jca 1120 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑖 ∈ ℤ)) |
73 | | elfzole1 13036 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑁 ≤ 𝑖) |
74 | 73 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑁 ≤ 𝑖) |
75 | 70 | zred 12076 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑚 ∈ ℝ) |
76 | | 1red 10631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 ∈ (𝑁...𝑚) → 1 ∈ ℝ) |
77 | 57, 76 | resubcld 11057 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 ∈ (𝑁...𝑚) → (𝑛 − 1) ∈ ℝ) |
78 | 69 | zred 12076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑚 ∈ ℝ) |
79 | 57 | ltm1d 11561 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 ∈ (𝑁...𝑚) → (𝑛 − 1) < 𝑛) |
80 | | elfzle2 12901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑛 ≤ 𝑚) |
81 | 77, 57, 78, 79, 80 | ltletrd 10789 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ (𝑁...𝑚) → (𝑛 − 1) < 𝑚) |
82 | 81 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑛 − 1) < 𝑚) |
83 | 55, 60, 75, 62, 82 | lelttrd 10787 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 < 𝑚) |
84 | 55, 75, 83 | ltled 10777 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ≤ 𝑚) |
85 | 72, 74, 84 | jca32 516 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → ((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑁 ≤ 𝑖 ∧ 𝑖 ≤ 𝑚))) |
86 | | elfz2 12889 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ (𝑁...𝑚) ↔ ((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑁 ≤ 𝑖 ∧ 𝑖 ≤ 𝑚))) |
87 | 85, 86 | sylibr 235 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ (𝑁...𝑚)) |
88 | 87 | adantlr 711 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ (𝑁...𝑚) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ (𝑁...𝑚)) |
89 | | rspa 3206 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑖 ∈
(𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)) ∧ 𝑖 ∈ (𝑁...𝑚)) → (𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) |
90 | 66, 88, 89 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ (𝑁...𝑚) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) |
91 | 90 | adantlll 714 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) |
92 | 65, 91 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → ¬ 𝑥 ∈ (𝐸‘𝑖)) |
93 | 92 | ex 413 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → (𝑖 ∈ (𝑁..^𝑛) → ¬ 𝑥 ∈ (𝐸‘𝑖))) |
94 | 52, 93 | ralrimi 3216 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → ∀𝑖 ∈ (𝑁..^𝑛) ¬ 𝑥 ∈ (𝐸‘𝑖)) |
95 | | ralnex 3236 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑖 ∈
(𝑁..^𝑛) ¬ 𝑥 ∈ (𝐸‘𝑖) ↔ ¬ ∃𝑖 ∈ (𝑁..^𝑛)𝑥 ∈ (𝐸‘𝑖)) |
96 | 94, 95 | sylib 219 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → ¬ ∃𝑖 ∈ (𝑁..^𝑛)𝑥 ∈ (𝐸‘𝑖)) |
97 | | eliun 4916 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ↔ ∃𝑖 ∈ (𝑁..^𝑛)𝑥 ∈ (𝐸‘𝑖)) |
98 | 96, 97 | sylnibr 330 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → ¬ 𝑥 ∈ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) |
99 | 98 | adantrl 712 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) → ¬ 𝑥 ∈ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) |
100 | 49, 99 | eldifd 3946 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) → 𝑥 ∈ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
101 | 14, 22 | syldan 591 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
102 | 101 | eqcomd 2827 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) = (𝐹‘𝑛)) |
103 | 102 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) = (𝐹‘𝑛)) |
104 | 100, 103 | eleqtrd 2915 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) → 𝑥 ∈ (𝐹‘𝑛)) |
105 | 104 | ex 413 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) → ((𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → 𝑥 ∈ (𝐹‘𝑛))) |
106 | 105 | ex 413 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 ∈ (𝑁...𝑚) → ((𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → 𝑥 ∈ (𝐹‘𝑛)))) |
107 | 4, 106 | reximdai 3311 |
. . . . . . 7
⊢ (𝜑 → (∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛))) |
108 | 107 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) → (∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛))) |
109 | 48, 108 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛)) |
110 | 109, 1 | sylibr 235 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) → 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)) |
111 | 39, 110 | eqelssd 3987 |
. . 3
⊢ (𝜑 → ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
112 | 111 | ralrimivw 3183 |
. 2
⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
113 | 11 | iuneqfzuz 41483 |
. . 3
⊢
(∀𝑚 ∈
𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) → ∪
𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
114 | 112, 113 | syl 17 |
. 2
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
115 | | fveq2 6664 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → (𝐸‘𝑛) = (𝐸‘𝑚)) |
116 | | oveq2 7153 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝑁..^𝑛) = (𝑁..^𝑚)) |
117 | 116 | iuneq1d 4938 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑁..^𝑚)(𝐸‘𝑖)) |
118 | 115, 117 | difeq12d 4099 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) = ((𝐸‘𝑚) ∖ ∪
𝑖 ∈ (𝑁..^𝑚)(𝐸‘𝑖))) |
119 | 118 | cbvmptv 5161 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) = (𝑚 ∈ 𝑍 ↦ ((𝐸‘𝑚) ∖ ∪
𝑖 ∈ (𝑁..^𝑚)(𝐸‘𝑖))) |
120 | 20, 119 | eqtri 2844 |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑚 ∈ 𝑍 ↦ ((𝐸‘𝑚) ∖ ∪
𝑖 ∈ (𝑁..^𝑚)(𝐸‘𝑖))) |
121 | | simpllr 772 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 < 𝑘) → 𝑛 ∈ 𝑍) |
122 | | simplr 765 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 < 𝑘) → 𝑘 ∈ 𝑍) |
123 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 < 𝑘) → 𝑛 < 𝑘) |
124 | 11, 120, 121, 122, 123 | iundjiunlem 42622 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 < 𝑘) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
125 | 124 | adantlr 711 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ 𝑛 < 𝑘) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
126 | | simpll 763 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → ((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍)) |
127 | | neqne 3024 |
. . . . . . . . . . . 12
⊢ (¬
𝑛 = 𝑘 → 𝑛 ≠ 𝑘) |
128 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ 𝑍) |
129 | 128, 11 | eleqtrdi 2923 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ (ℤ≥‘𝑁)) |
130 | | eluzelz 12242 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → 𝑘 ∈ ℤ) |
131 | 129, 130 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ) |
132 | 131 | zred 12076 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℝ) |
133 | 132 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℝ) |
134 | 133 | ad2antrr 722 |
. . . . . . . . . . . . 13
⊢ ((((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 ≠ 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 ∈ ℝ) |
135 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍) |
136 | 135, 11 | eleqtrdi 2923 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ≥‘𝑁)) |
137 | | eluzelz 12242 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘𝑁) → 𝑛 ∈ ℤ) |
138 | 136, 137 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ) |
139 | 138 | zred 12076 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℝ) |
140 | 139 | ad3antrrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 ≠ 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑛 ∈ ℝ) |
141 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 < 𝑘) → ¬ 𝑛 < 𝑘) |
142 | 133 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 < 𝑘) → 𝑘 ∈ ℝ) |
143 | 139 | ad2antrr 722 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 < 𝑘) → 𝑛 ∈ ℝ) |
144 | 142, 143 | lenltd 10775 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 < 𝑘) → (𝑘 ≤ 𝑛 ↔ ¬ 𝑛 < 𝑘)) |
145 | 141, 144 | mpbird 258 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 < 𝑘) → 𝑘 ≤ 𝑛) |
146 | 145 | adantlr 711 |
. . . . . . . . . . . . 13
⊢ ((((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 ≠ 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 ≤ 𝑛) |
147 | | simplr 765 |
. . . . . . . . . . . . 13
⊢ ((((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 ≠ 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑛 ≠ 𝑘) |
148 | 134, 140,
146, 147 | leneltd 10783 |
. . . . . . . . . . . 12
⊢ ((((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 ≠ 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 < 𝑛) |
149 | 127, 148 | sylanl2 677 |
. . . . . . . . . . 11
⊢ ((((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 < 𝑛) |
150 | 149 | ad5ant2345 1362 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 < 𝑛) |
151 | | anass 469 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ↔ (𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍))) |
152 | | incom 4177 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ((𝐹‘𝑘) ∩ (𝐹‘𝑛)) |
153 | 152 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍)) ∧ 𝑘 < 𝑛) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ((𝐹‘𝑘) ∩ (𝐹‘𝑛))) |
154 | | simplrr 774 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍)) ∧ 𝑘 < 𝑛) → 𝑘 ∈ 𝑍) |
155 | | simplrl 773 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍)) ∧ 𝑘 < 𝑛) → 𝑛 ∈ 𝑍) |
156 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍)) ∧ 𝑘 < 𝑛) → 𝑘 < 𝑛) |
157 | 11, 120, 154, 155, 156 | iundjiunlem 42622 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍)) ∧ 𝑘 < 𝑛) → ((𝐹‘𝑘) ∩ (𝐹‘𝑛)) = ∅) |
158 | 153, 157 | eqtrd 2856 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍)) ∧ 𝑘 < 𝑛) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
159 | 151, 158 | sylanb 581 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ 𝑘 < 𝑛) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
160 | 126, 150,
159 | syl2anc 584 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
161 | 125, 160 | pm2.61dan 809 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 = 𝑘) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
162 | 161 | ex 413 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (¬ 𝑛 = 𝑘 → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
163 | | df-or 842 |
. . . . . . 7
⊢ ((𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) ↔ (¬ 𝑛 = 𝑘 → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
164 | 162, 163 | sylibr 235 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
165 | 164 | ralrimiva 3182 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
166 | 165 | ex 413 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ 𝑍 → ∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅))) |
167 | 4, 166 | ralrimi 3216 |
. . 3
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 ∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
168 | | nfcv 2977 |
. . . . 5
⊢
Ⅎ𝑚(𝐹‘𝑛) |
169 | | nfmpt1 5156 |
. . . . . . 7
⊢
Ⅎ𝑛(𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
170 | 20, 169 | nfcxfr 2975 |
. . . . . 6
⊢
Ⅎ𝑛𝐹 |
171 | | nfcv 2977 |
. . . . . 6
⊢
Ⅎ𝑛𝑚 |
172 | 170, 171 | nffv 6674 |
. . . . 5
⊢
Ⅎ𝑛(𝐹‘𝑚) |
173 | | fveq2 6664 |
. . . . 5
⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚)) |
174 | 168, 172,
173 | cbvdisj 5033 |
. . . 4
⊢
(Disj 𝑛
∈ 𝑍 (𝐹‘𝑛) ↔ Disj 𝑚 ∈ 𝑍 (𝐹‘𝑚)) |
175 | | fveq2 6664 |
. . . . 5
⊢ (𝑚 = 𝑘 → (𝐹‘𝑚) = (𝐹‘𝑘)) |
176 | 175 | disjor 5038 |
. . . 4
⊢
(Disj 𝑚
∈ 𝑍 (𝐹‘𝑚) ↔ ∀𝑚 ∈ 𝑍 ∀𝑘 ∈ 𝑍 (𝑚 = 𝑘 ∨ ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅)) |
177 | | nfcv 2977 |
. . . . . 6
⊢
Ⅎ𝑛𝑍 |
178 | | nfv 1906 |
. . . . . . 7
⊢
Ⅎ𝑛 𝑚 = 𝑘 |
179 | | nfcv 2977 |
. . . . . . . . . 10
⊢
Ⅎ𝑛𝑘 |
180 | 170, 179 | nffv 6674 |
. . . . . . . . 9
⊢
Ⅎ𝑛(𝐹‘𝑘) |
181 | 172, 180 | nfin 4192 |
. . . . . . . 8
⊢
Ⅎ𝑛((𝐹‘𝑚) ∩ (𝐹‘𝑘)) |
182 | | nfcv 2977 |
. . . . . . . 8
⊢
Ⅎ𝑛∅ |
183 | 181, 182 | nfeq 2991 |
. . . . . . 7
⊢
Ⅎ𝑛((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅ |
184 | 178, 183 | nfor 1896 |
. . . . . 6
⊢
Ⅎ𝑛(𝑚 = 𝑘 ∨ ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅) |
185 | 177, 184 | nfral 3226 |
. . . . 5
⊢
Ⅎ𝑛∀𝑘 ∈ 𝑍 (𝑚 = 𝑘 ∨ ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅) |
186 | | nfv 1906 |
. . . . 5
⊢
Ⅎ𝑚∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
187 | | equequ1 2023 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (𝑚 = 𝑘 ↔ 𝑛 = 𝑘)) |
188 | | fveq2 6664 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
189 | 188 | ineq1d 4187 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ((𝐹‘𝑛) ∩ (𝐹‘𝑘))) |
190 | 189 | eqeq1d 2823 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅ ↔ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
191 | 187, 190 | orbi12d 912 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((𝑚 = 𝑘 ∨ ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅) ↔ (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅))) |
192 | 191 | ralbidv 3197 |
. . . . 5
⊢ (𝑚 = 𝑛 → (∀𝑘 ∈ 𝑍 (𝑚 = 𝑘 ∨ ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅) ↔ ∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅))) |
193 | 185, 186,
192 | cbvral 3446 |
. . . 4
⊢
(∀𝑚 ∈
𝑍 ∀𝑘 ∈ 𝑍 (𝑚 = 𝑘 ∨ ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅) ↔ ∀𝑛 ∈ 𝑍 ∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
194 | 174, 176,
193 | 3bitri 298 |
. . 3
⊢
(Disj 𝑛
∈ 𝑍 (𝐹‘𝑛) ↔ ∀𝑛 ∈ 𝑍 ∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
195 | 167, 194 | sylibr 235 |
. 2
⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛)) |
196 | 112, 114,
195 | jca31 515 |
1
⊢ (𝜑 → ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ ∪
𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∧ Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛))) |