| Step | Hyp | Ref
| Expression |
| 1 | | eliun 4995 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) ↔ ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛)) |
| 2 | 1 | biimpi 216 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛)) |
| 3 | 2 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛)) |
| 4 | | iundjiun.nph |
. . . . . . . . 9
⊢
Ⅎ𝑛𝜑 |
| 5 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑛𝑥 |
| 6 | | nfiu1 5027 |
. . . . . . . . . 10
⊢
Ⅎ𝑛∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) |
| 7 | 5, 6 | nfel 2920 |
. . . . . . . . 9
⊢
Ⅎ𝑛 𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) |
| 8 | | simp2 1138 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹‘𝑛)) → 𝑛 ∈ (𝑁...𝑚)) |
| 9 | | simpl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) → 𝜑) |
| 10 | | elfzuz 13560 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ (ℤ≥‘𝑁)) |
| 11 | | iundjiun.z |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑍 =
(ℤ≥‘𝑁) |
| 12 | 11 | eqcomi 2746 |
. . . . . . . . . . . . . . . . 17
⊢
(ℤ≥‘𝑁) = 𝑍 |
| 13 | 10, 12 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ 𝑍) |
| 14 | 13 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) → 𝑛 ∈ 𝑍) |
| 15 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) |
| 16 | | iundjiun.e |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐸:𝑍⟶𝑉) |
| 17 | 16 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ 𝑉) |
| 18 | 17 | difexd 5331 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) |
| 19 | | iundjiun.f |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
| 20 | 19 | fvmpt2 7027 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ 𝑍 ∧ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
| 21 | 15, 18, 20 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
| 22 | | difssd 4137 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ⊆ (𝐸‘𝑛)) |
| 23 | 21, 22 | eqsstrd 4018 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ⊆ (𝐸‘𝑛)) |
| 24 | 9, 14, 23 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) → (𝐹‘𝑛) ⊆ (𝐸‘𝑛)) |
| 25 | 24 | 3adant3 1133 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹‘𝑛)) → (𝐹‘𝑛) ⊆ (𝐸‘𝑛)) |
| 26 | | simp3 1139 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹‘𝑛)) → 𝑥 ∈ (𝐹‘𝑛)) |
| 27 | 25, 26 | sseldd 3984 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹‘𝑛)) → 𝑥 ∈ (𝐸‘𝑛)) |
| 28 | | rspe 3249 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐸‘𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸‘𝑛)) |
| 29 | 8, 27, 28 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹‘𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸‘𝑛)) |
| 30 | | eliun 4995 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ↔ ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸‘𝑛)) |
| 31 | 29, 30 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚) ∧ 𝑥 ∈ (𝐹‘𝑛)) → 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
| 32 | 31 | 3exp 1120 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ (𝑁...𝑚) → (𝑥 ∈ (𝐹‘𝑛) → 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)))) |
| 33 | 4, 7, 32 | rexlimd 3266 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛) → 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))) |
| 34 | 33 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)) → (∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛) → 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))) |
| 35 | 3, 34 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)) → 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
| 36 | 35 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
| 37 | | dfss3 3972 |
. . . . 5
⊢ (∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) ⊆ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ↔ ∀𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
| 38 | 36, 37 | sylibr 234 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) ⊆ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
| 39 | | fzssuz 13605 |
. . . . . . . . 9
⊢ (𝑁...𝑚) ⊆ (ℤ≥‘𝑁) |
| 40 | 39 | a1i 11 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) → (𝑁...𝑚) ⊆ (ℤ≥‘𝑁)) |
| 41 | 30 | biimpi 216 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸‘𝑛)) |
| 42 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑛 𝑥 ∈ (𝐸‘𝑖) |
| 43 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑖 → (𝐸‘𝑛) = (𝐸‘𝑖)) |
| 44 | 43 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑛 = 𝑖 → (𝑥 ∈ (𝐸‘𝑛) ↔ 𝑥 ∈ (𝐸‘𝑖))) |
| 45 | 42, 44 | uzwo4 45058 |
. . . . . . . 8
⊢ (((𝑁...𝑚) ⊆ (ℤ≥‘𝑁) ∧ ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐸‘𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) |
| 46 | 40, 41, 45 | syl2anc 584 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) → ∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) |
| 47 | 46 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) |
| 48 | | simprl 771 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) → 𝑥 ∈ (𝐸‘𝑛)) |
| 49 | | nfv 1914 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑖(𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) |
| 50 | | nfra1 3284 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑖∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)) |
| 51 | 49, 50 | nfan 1899 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑖((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) |
| 52 | | elfzoelz 13699 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ ℤ) |
| 53 | 52 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ ℝ) |
| 54 | 53 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ ℝ) |
| 55 | | elfzelz 13564 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ ℤ) |
| 56 | 55 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑛 ∈ ℝ) |
| 57 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑛 ∈ ℝ) |
| 58 | | 1red 11262 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 1 ∈ ℝ) |
| 59 | 57, 58 | resubcld 11691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑛 − 1) ∈ ℝ) |
| 60 | | elfzolem1 13744 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ≤ (𝑛 − 1)) |
| 61 | 60 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ≤ (𝑛 − 1)) |
| 62 | 57 | ltm1d 12200 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑛 − 1) < 𝑛) |
| 63 | 54, 59, 57, 61, 62 | lelttrd 11419 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 < 𝑛) |
| 64 | 63 | ad4ant24 754 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 < 𝑛) |
| 65 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ (𝑁...𝑚) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) |
| 66 | | elfzel1 13563 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑁 ∈ ℤ) |
| 67 | 66 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑁 ∈ ℤ) |
| 68 | | elfzel2 13562 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑚 ∈ ℤ) |
| 69 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑚 ∈ ℤ) |
| 70 | 52 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ ℤ) |
| 71 | | elfzole1 13707 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑁 ≤ 𝑖) |
| 72 | 71 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑁 ≤ 𝑖) |
| 73 | 69 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑚 ∈ ℝ) |
| 74 | | 1red 11262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 ∈ (𝑁...𝑚) → 1 ∈ ℝ) |
| 75 | 56, 74 | resubcld 11691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ (𝑁...𝑚) → (𝑛 − 1) ∈ ℝ) |
| 76 | 68 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑚 ∈ ℝ) |
| 77 | 56 | ltm1d 12200 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ (𝑁...𝑚) → (𝑛 − 1) < 𝑛) |
| 78 | | elfzle2 13568 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ (𝑁...𝑚) → 𝑛 ≤ 𝑚) |
| 79 | 75, 56, 76, 77, 78 | ltletrd 11421 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ (𝑁...𝑚) → (𝑛 − 1) < 𝑚) |
| 80 | 79 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑛 − 1) < 𝑚) |
| 81 | 54, 59, 73, 61, 80 | lelttrd 11419 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 < 𝑚) |
| 82 | 54, 73, 81 | ltled 11409 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ≤ 𝑚) |
| 83 | 67, 69, 70, 72, 82 | elfzd 13555 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ (𝑁...𝑚) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ (𝑁...𝑚)) |
| 84 | 83 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ (𝑁...𝑚) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ (𝑁...𝑚)) |
| 85 | | rspa 3248 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑖 ∈
(𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)) ∧ 𝑖 ∈ (𝑁...𝑚)) → (𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) |
| 86 | 65, 84, 85 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ (𝑁...𝑚) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) |
| 87 | 86 | adantlll 718 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) |
| 88 | 64, 87 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) ∧ 𝑖 ∈ (𝑁..^𝑛)) → ¬ 𝑥 ∈ (𝐸‘𝑖)) |
| 89 | 88 | ex 412 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → (𝑖 ∈ (𝑁..^𝑛) → ¬ 𝑥 ∈ (𝐸‘𝑖))) |
| 90 | 51, 89 | ralrimi 3257 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → ∀𝑖 ∈ (𝑁..^𝑛) ¬ 𝑥 ∈ (𝐸‘𝑖)) |
| 91 | | ralnex 3072 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑖 ∈
(𝑁..^𝑛) ¬ 𝑥 ∈ (𝐸‘𝑖) ↔ ¬ ∃𝑖 ∈ (𝑁..^𝑛)𝑥 ∈ (𝐸‘𝑖)) |
| 92 | 90, 91 | sylib 218 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → ¬ ∃𝑖 ∈ (𝑁..^𝑛)𝑥 ∈ (𝐸‘𝑖)) |
| 93 | | eliun 4995 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ↔ ∃𝑖 ∈ (𝑁..^𝑛)𝑥 ∈ (𝐸‘𝑖)) |
| 94 | 92, 93 | sylnibr 329 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → ¬ 𝑥 ∈ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) |
| 95 | 94 | adantrl 716 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) → ¬ 𝑥 ∈ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) |
| 96 | 48, 95 | eldifd 3962 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) → 𝑥 ∈ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
| 97 | 14, 21 | syldan 591 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
| 98 | 97 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) = (𝐹‘𝑛)) |
| 99 | 98 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) = (𝐹‘𝑛)) |
| 100 | 96, 99 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) ∧ (𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖)))) → 𝑥 ∈ (𝐹‘𝑛)) |
| 101 | 100 | ex 412 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑁...𝑚)) → ((𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → 𝑥 ∈ (𝐹‘𝑛))) |
| 102 | 101 | ex 412 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 ∈ (𝑁...𝑚) → ((𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → 𝑥 ∈ (𝐹‘𝑛)))) |
| 103 | 4, 102 | reximdai 3261 |
. . . . . . 7
⊢ (𝜑 → (∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛))) |
| 104 | 103 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) → (∃𝑛 ∈ (𝑁...𝑚)(𝑥 ∈ (𝐸‘𝑛) ∧ ∀𝑖 ∈ (𝑁...𝑚)(𝑖 < 𝑛 → ¬ 𝑥 ∈ (𝐸‘𝑖))) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛))) |
| 105 | 47, 104 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) → ∃𝑛 ∈ (𝑁...𝑚)𝑥 ∈ (𝐹‘𝑛)) |
| 106 | 105, 1 | sylibr 234 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) → 𝑥 ∈ ∪
𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)) |
| 107 | 38, 106 | eqelssd 4005 |
. . 3
⊢ (𝜑 → ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
| 108 | 107 | ralrimivw 3150 |
. 2
⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛)) |
| 109 | 11 | iuneqfzuz 45346 |
. . 3
⊢
(∀𝑚 ∈
𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) → ∪
𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
| 110 | 108, 109 | syl 17 |
. 2
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
| 111 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → (𝐸‘𝑛) = (𝐸‘𝑚)) |
| 112 | | oveq2 7439 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝑁..^𝑛) = (𝑁..^𝑚)) |
| 113 | 112 | iuneq1d 5019 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑁..^𝑚)(𝐸‘𝑖)) |
| 114 | 111, 113 | difeq12d 4127 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) = ((𝐸‘𝑚) ∖ ∪
𝑖 ∈ (𝑁..^𝑚)(𝐸‘𝑖))) |
| 115 | 114 | cbvmptv 5255 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) = (𝑚 ∈ 𝑍 ↦ ((𝐸‘𝑚) ∖ ∪
𝑖 ∈ (𝑁..^𝑚)(𝐸‘𝑖))) |
| 116 | 19, 115 | eqtri 2765 |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑚 ∈ 𝑍 ↦ ((𝐸‘𝑚) ∖ ∪
𝑖 ∈ (𝑁..^𝑚)(𝐸‘𝑖))) |
| 117 | | simpllr 776 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 < 𝑘) → 𝑛 ∈ 𝑍) |
| 118 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 < 𝑘) → 𝑘 ∈ 𝑍) |
| 119 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 < 𝑘) → 𝑛 < 𝑘) |
| 120 | 11, 116, 117, 118, 119 | iundjiunlem 46474 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 < 𝑘) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
| 121 | 120 | adantlr 715 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ 𝑛 < 𝑘) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
| 122 | | simpll 767 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → ((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍)) |
| 123 | | neqne 2948 |
. . . . . . . . . . . 12
⊢ (¬
𝑛 = 𝑘 → 𝑛 ≠ 𝑘) |
| 124 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ 𝑍) |
| 125 | 124, 11 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ (ℤ≥‘𝑁)) |
| 126 | | eluzelz 12888 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → 𝑘 ∈ ℤ) |
| 127 | 125, 126 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ) |
| 128 | 127 | zred 12722 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℝ) |
| 129 | 128 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℝ) |
| 130 | 129 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 ≠ 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 ∈ ℝ) |
| 131 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍) |
| 132 | 131, 11 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ≥‘𝑁)) |
| 133 | | eluzelz 12888 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘𝑁) → 𝑛 ∈ ℤ) |
| 134 | 132, 133 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ) |
| 135 | 134 | zred 12722 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℝ) |
| 136 | 135 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 ≠ 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑛 ∈ ℝ) |
| 137 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 < 𝑘) → ¬ 𝑛 < 𝑘) |
| 138 | 129 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 < 𝑘) → 𝑘 ∈ ℝ) |
| 139 | 135 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 < 𝑘) → 𝑛 ∈ ℝ) |
| 140 | 138, 139 | lenltd 11407 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 < 𝑘) → (𝑘 ≤ 𝑛 ↔ ¬ 𝑛 < 𝑘)) |
| 141 | 137, 140 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 < 𝑘) → 𝑘 ≤ 𝑛) |
| 142 | 141 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ ((((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 ≠ 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 ≤ 𝑛) |
| 143 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ ((((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 ≠ 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑛 ≠ 𝑘) |
| 144 | 130, 136,
142, 143 | leneltd 11415 |
. . . . . . . . . . . 12
⊢ ((((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 ≠ 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 < 𝑛) |
| 145 | 123, 144 | sylanl2 681 |
. . . . . . . . . . 11
⊢ ((((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 < 𝑛) |
| 146 | 145 | ad5ant2345 1372 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → 𝑘 < 𝑛) |
| 147 | | anass 468 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ↔ (𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍))) |
| 148 | | incom 4209 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ((𝐹‘𝑘) ∩ (𝐹‘𝑛)) |
| 149 | 148 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍)) ∧ 𝑘 < 𝑛) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ((𝐹‘𝑘) ∩ (𝐹‘𝑛))) |
| 150 | | simplrr 778 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍)) ∧ 𝑘 < 𝑛) → 𝑘 ∈ 𝑍) |
| 151 | | simplrl 777 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍)) ∧ 𝑘 < 𝑛) → 𝑛 ∈ 𝑍) |
| 152 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍)) ∧ 𝑘 < 𝑛) → 𝑘 < 𝑛) |
| 153 | 11, 116, 150, 151, 152 | iundjiunlem 46474 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍)) ∧ 𝑘 < 𝑛) → ((𝐹‘𝑘) ∩ (𝐹‘𝑛)) = ∅) |
| 154 | 149, 153 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍)) ∧ 𝑘 < 𝑛) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
| 155 | 147, 154 | sylanb 581 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ 𝑘 < 𝑛) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
| 156 | 122, 146,
155 | syl2anc 584 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 = 𝑘) ∧ ¬ 𝑛 < 𝑘) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
| 157 | 121, 156 | pm2.61dan 813 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ¬ 𝑛 = 𝑘) → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
| 158 | 157 | ex 412 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (¬ 𝑛 = 𝑘 → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
| 159 | | df-or 849 |
. . . . . . 7
⊢ ((𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) ↔ (¬ 𝑛 = 𝑘 → ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
| 160 | 158, 159 | sylibr 234 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
| 161 | 160 | ralrimiva 3146 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
| 162 | 161 | ex 412 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ 𝑍 → ∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅))) |
| 163 | 4, 162 | ralrimi 3257 |
. . 3
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 ∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
| 164 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑚(𝐹‘𝑛) |
| 165 | | nfmpt1 5250 |
. . . . . . 7
⊢
Ⅎ𝑛(𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
| 166 | 19, 165 | nfcxfr 2903 |
. . . . . 6
⊢
Ⅎ𝑛𝐹 |
| 167 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑛𝑚 |
| 168 | 166, 167 | nffv 6916 |
. . . . 5
⊢
Ⅎ𝑛(𝐹‘𝑚) |
| 169 | | fveq2 6906 |
. . . . 5
⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚)) |
| 170 | 164, 168,
169 | cbvdisj 5120 |
. . . 4
⊢
(Disj 𝑛
∈ 𝑍 (𝐹‘𝑛) ↔ Disj 𝑚 ∈ 𝑍 (𝐹‘𝑚)) |
| 171 | | fveq2 6906 |
. . . . 5
⊢ (𝑚 = 𝑘 → (𝐹‘𝑚) = (𝐹‘𝑘)) |
| 172 | 171 | disjor 5125 |
. . . 4
⊢
(Disj 𝑚
∈ 𝑍 (𝐹‘𝑚) ↔ ∀𝑚 ∈ 𝑍 ∀𝑘 ∈ 𝑍 (𝑚 = 𝑘 ∨ ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅)) |
| 173 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑛𝑍 |
| 174 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑛 𝑚 = 𝑘 |
| 175 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑛𝑘 |
| 176 | 166, 175 | nffv 6916 |
. . . . . . . . 9
⊢
Ⅎ𝑛(𝐹‘𝑘) |
| 177 | 168, 176 | nfin 4224 |
. . . . . . . 8
⊢
Ⅎ𝑛((𝐹‘𝑚) ∩ (𝐹‘𝑘)) |
| 178 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑛∅ |
| 179 | 177, 178 | nfeq 2919 |
. . . . . . 7
⊢
Ⅎ𝑛((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅ |
| 180 | 174, 179 | nfor 1904 |
. . . . . 6
⊢
Ⅎ𝑛(𝑚 = 𝑘 ∨ ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅) |
| 181 | 173, 180 | nfralw 3311 |
. . . . 5
⊢
Ⅎ𝑛∀𝑘 ∈ 𝑍 (𝑚 = 𝑘 ∨ ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅) |
| 182 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑚∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅) |
| 183 | | equequ1 2024 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (𝑚 = 𝑘 ↔ 𝑛 = 𝑘)) |
| 184 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
| 185 | 184 | ineq1d 4219 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ((𝐹‘𝑛) ∩ (𝐹‘𝑘))) |
| 186 | 185 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅ ↔ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
| 187 | 183, 186 | orbi12d 919 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((𝑚 = 𝑘 ∨ ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅) ↔ (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅))) |
| 188 | 187 | ralbidv 3178 |
. . . . 5
⊢ (𝑚 = 𝑛 → (∀𝑘 ∈ 𝑍 (𝑚 = 𝑘 ∨ ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅) ↔ ∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅))) |
| 189 | 181, 182,
188 | cbvralw 3306 |
. . . 4
⊢
(∀𝑚 ∈
𝑍 ∀𝑘 ∈ 𝑍 (𝑚 = 𝑘 ∨ ((𝐹‘𝑚) ∩ (𝐹‘𝑘)) = ∅) ↔ ∀𝑛 ∈ 𝑍 ∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
| 190 | 170, 172,
189 | 3bitri 297 |
. . 3
⊢
(Disj 𝑛
∈ 𝑍 (𝐹‘𝑛) ↔ ∀𝑛 ∈ 𝑍 ∀𝑘 ∈ 𝑍 (𝑛 = 𝑘 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑘)) = ∅)) |
| 191 | 163, 190 | sylibr 234 |
. 2
⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛)) |
| 192 | 108, 110,
191 | jca31 514 |
1
⊢ (𝜑 → ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ ∪
𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∧ Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛))) |