| Step | Hyp | Ref
| Expression |
| 1 | | iftrue 4531 |
. . . . . . . 8
⊢ ((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = ∅) |
| 2 | 1 | adantl 481 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = ∅) |
| 3 | | 0ex 5307 |
. . . . . . . . 9
⊢ ∅
∈ V |
| 4 | 3 | snid 4662 |
. . . . . . . 8
⊢ ∅
∈ {∅} |
| 5 | | elun2 4183 |
. . . . . . . 8
⊢ (∅
∈ {∅} → ∅ ∈ (𝑋 ∪ {∅})) |
| 6 | 4, 5 | ax-mp 5 |
. . . . . . 7
⊢ ∅
∈ (𝑋 ∪
{∅}) |
| 7 | 2, 6 | eqeltrdi 2849 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅})) |
| 8 | 7 | adantll 714 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅})) |
| 9 | | iffalse 4534 |
. . . . . . 7
⊢ (¬
(𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑛 − 1))) |
| 10 | 9 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑛 − 1))) |
| 11 | | nnfoctbdjlem.g |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺:𝐴–1-1-onto→𝑋) |
| 12 | | f1of 6848 |
. . . . . . . . . . 11
⊢ (𝐺:𝐴–1-1-onto→𝑋 → 𝐺:𝐴⟶𝑋) |
| 13 | 11, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:𝐴⟶𝑋) |
| 14 | 13 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → 𝐺:𝐴⟶𝑋) |
| 15 | | pm2.46 883 |
. . . . . . . . . . 11
⊢ (¬
(𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → ¬ ¬ (𝑛 − 1) ∈ 𝐴) |
| 16 | 15 | notnotrd 133 |
. . . . . . . . . 10
⊢ (¬
(𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → (𝑛 − 1) ∈ 𝐴) |
| 17 | 16 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝑛 − 1) ∈ 𝐴) |
| 18 | 14, 17 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ 𝑋) |
| 19 | 18 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ 𝑋) |
| 20 | | elun1 4182 |
. . . . . . 7
⊢ ((𝐺‘(𝑛 − 1)) ∈ 𝑋 → (𝐺‘(𝑛 − 1)) ∈ (𝑋 ∪ {∅})) |
| 21 | 19, 20 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ (𝑋 ∪ {∅})) |
| 22 | 10, 21 | eqeltrd 2841 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅})) |
| 23 | 8, 22 | pm2.61dan 813 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅})) |
| 24 | | nnfoctbdjlem.f |
. . . 4
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))) |
| 25 | 23, 24 | fmptd 7134 |
. . 3
⊢ (𝜑 → 𝐹:ℕ⟶(𝑋 ∪ {∅})) |
| 26 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
| 27 | | f1ofo 6855 |
. . . . . . . . . . . . 13
⊢ (𝐺:𝐴–1-1-onto→𝑋 → 𝐺:𝐴–onto→𝑋) |
| 28 | | forn 6823 |
. . . . . . . . . . . . 13
⊢ (𝐺:𝐴–onto→𝑋 → ran 𝐺 = 𝑋) |
| 29 | 11, 27, 28 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝐺 = 𝑋) |
| 30 | 29 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 = ran 𝐺) |
| 31 | 30 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑋 = ran 𝐺) |
| 32 | 26, 31 | eleqtrd 2843 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ ran 𝐺) |
| 33 | 13 | ffnd 6737 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 Fn 𝐴) |
| 34 | | fvelrnb 6969 |
. . . . . . . . . . 11
⊢ (𝐺 Fn 𝐴 → (𝑦 ∈ ran 𝐺 ↔ ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦)) |
| 35 | 33, 34 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ ran 𝐺 ↔ ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦)) |
| 36 | 35 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑦 ∈ ran 𝐺 ↔ ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦)) |
| 37 | 32, 36 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦) |
| 38 | | nnfoctbdjlem.a |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ⊆ ℕ) |
| 39 | 38 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℕ) |
| 40 | 39 | peano2nnd 12283 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑘 + 1) ∈ ℕ) |
| 41 | 40 | 3adant3 1133 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝑘 + 1) ∈ ℕ) |
| 42 | 24 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))))) |
| 43 | | 1red 11262 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 1 ∈
ℝ) |
| 44 | | 1red 11262 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℝ) |
| 45 | 39 | nnrpd 13075 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℝ+) |
| 46 | 44, 45 | ltaddrp2d 13111 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 < (𝑘 + 1)) |
| 47 | 46 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 1 < (𝑘 + 1)) |
| 48 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = (𝑘 + 1) → 𝑛 = (𝑘 + 1)) |
| 49 | 48 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = (𝑘 + 1) → (𝑘 + 1) = 𝑛) |
| 50 | 49 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝑘 + 1) = 𝑛) |
| 51 | 47, 50 | breqtrd 5169 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 1 < 𝑛) |
| 52 | 43, 51 | gtned 11396 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 𝑛 ≠ 1) |
| 53 | 52 | neneqd 2945 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → ¬ 𝑛 = 1) |
| 54 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = (𝑘 + 1) → (𝑛 − 1) = ((𝑘 + 1) − 1)) |
| 55 | 39 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℂ) |
| 56 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℂ) |
| 57 | 55, 56 | pncand 11621 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 + 1) − 1) = 𝑘) |
| 58 | 54, 57 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝑛 − 1) = 𝑘) |
| 59 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 𝑘 ∈ 𝐴) |
| 60 | 58, 59 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝑛 − 1) ∈ 𝐴) |
| 61 | 60 | notnotd 144 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → ¬ ¬ (𝑛 − 1) ∈ 𝐴) |
| 62 | | ioran 986 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
(𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ↔ (¬ 𝑛 = 1 ∧ ¬ ¬ (𝑛 − 1) ∈ 𝐴)) |
| 63 | 53, 61, 62 | sylanbrc 583 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) |
| 64 | 63 | iffalsed 4536 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑛 − 1))) |
| 65 | 58 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝐺‘(𝑛 − 1)) = (𝐺‘𝑘)) |
| 66 | 64, 65 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘𝑘)) |
| 67 | 13 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘𝑘) ∈ 𝑋) |
| 68 | 42, 66, 40, 67 | fvmptd 7023 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘(𝑘 + 1)) = (𝐺‘𝑘)) |
| 69 | 68 | 3adant3 1133 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝐹‘(𝑘 + 1)) = (𝐺‘𝑘)) |
| 70 | | simp3 1139 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝐺‘𝑘) = 𝑦) |
| 71 | 69, 70 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝐹‘(𝑘 + 1)) = 𝑦) |
| 72 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑘 + 1) → (𝐹‘𝑚) = (𝐹‘(𝑘 + 1))) |
| 73 | 72 | eqeq1d 2739 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑘 + 1) → ((𝐹‘𝑚) = 𝑦 ↔ (𝐹‘(𝑘 + 1)) = 𝑦)) |
| 74 | 73 | rspcev 3622 |
. . . . . . . . . . . 12
⊢ (((𝑘 + 1) ∈ ℕ ∧
(𝐹‘(𝑘 + 1)) = 𝑦) → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦) |
| 75 | 41, 71, 74 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦) |
| 76 | 75 | 3exp 1120 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ 𝐴 → ((𝐺‘𝑘) = 𝑦 → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦))) |
| 77 | 76 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑘 ∈ 𝐴 → ((𝐺‘𝑘) = 𝑦 → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦))) |
| 78 | 77 | rexlimdv 3153 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦 → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)) |
| 79 | 37, 78 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦) |
| 80 | | id 22 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑚) = 𝑦 → (𝐹‘𝑚) = 𝑦) |
| 81 | 80 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝐹‘𝑚) = 𝑦 → 𝑦 = (𝐹‘𝑚)) |
| 82 | 81 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑚 ∈ ℕ) → ((𝐹‘𝑚) = 𝑦 → 𝑦 = (𝐹‘𝑚))) |
| 83 | 82 | reximdva 3168 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦 → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))) |
| 84 | 79, 83 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)) |
| 85 | 84 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)) |
| 86 | | simpll 767 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ ¬ 𝑦 ∈ 𝑋) → 𝜑) |
| 87 | | elunnel1 4154 |
. . . . . . . 8
⊢ ((𝑦 ∈ (𝑋 ∪ {∅}) ∧ ¬ 𝑦 ∈ 𝑋) → 𝑦 ∈ {∅}) |
| 88 | | elsni 4643 |
. . . . . . . 8
⊢ (𝑦 ∈ {∅} → 𝑦 = ∅) |
| 89 | 87, 88 | syl 17 |
. . . . . . 7
⊢ ((𝑦 ∈ (𝑋 ∪ {∅}) ∧ ¬ 𝑦 ∈ 𝑋) → 𝑦 = ∅) |
| 90 | 89 | adantll 714 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ ¬ 𝑦 ∈ 𝑋) → 𝑦 = ∅) |
| 91 | | 1nn 12277 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
| 92 | 91 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = ∅) → 1 ∈
ℕ) |
| 93 | 1 | orcs 876 |
. . . . . . . . . 10
⊢ (𝑛 = 1 → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = ∅) |
| 94 | 91 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℕ) |
| 95 | 3 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ∅ ∈
V) |
| 96 | 24, 93, 94, 95 | fvmptd3 7039 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘1) = ∅) |
| 97 | 96 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = ∅) → (𝐹‘1) = ∅) |
| 98 | | id 22 |
. . . . . . . . . 10
⊢ (𝑦 = ∅ → 𝑦 = ∅) |
| 99 | 98 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝑦 = ∅ → ∅ =
𝑦) |
| 100 | 99 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = ∅) → ∅ = 𝑦) |
| 101 | 97, 100 | eqtr2d 2778 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = ∅) → 𝑦 = (𝐹‘1)) |
| 102 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑚 = 1 → (𝐹‘𝑚) = (𝐹‘1)) |
| 103 | 102 | rspceeqv 3645 |
. . . . . . 7
⊢ ((1
∈ ℕ ∧ 𝑦 =
(𝐹‘1)) →
∃𝑚 ∈ ℕ
𝑦 = (𝐹‘𝑚)) |
| 104 | 92, 101, 103 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = ∅) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)) |
| 105 | 86, 90, 104 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ ¬ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)) |
| 106 | 85, 105 | pm2.61dan 813 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)) |
| 107 | 106 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ (𝑋 ∪ {∅})∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)) |
| 108 | | dffo3 7122 |
. . 3
⊢ (𝐹:ℕ–onto→(𝑋 ∪ {∅}) ↔ (𝐹:ℕ⟶(𝑋 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑋 ∪ {∅})∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))) |
| 109 | 25, 107, 108 | sylanbrc 583 |
. 2
⊢ (𝜑 → 𝐹:ℕ–onto→(𝑋 ∪ {∅})) |
| 110 | | animorrl 983 |
. . . . 5
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 = 𝑚) → (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)) |
| 111 | 2, 3 | eqeltrdi 2849 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ V) |
| 112 | 24 | fvmpt2 7027 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ V) → (𝐹‘𝑛) = if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))) |
| 113 | 111, 112 | syldan 591 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))) |
| 114 | 113, 2 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = ∅) |
| 115 | 114 | ineq1d 4219 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = (∅ ∩ (𝐹‘𝑚))) |
| 116 | | 0in 4397 |
. . . . . . . . . 10
⊢ (∅
∩ (𝐹‘𝑚)) = ∅ |
| 117 | 115, 116 | eqtrdi 2793 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅) |
| 118 | 117 | adantlr 715 |
. . . . . . . 8
⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅) |
| 119 | 118 | ad4ant24 754 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅) |
| 120 | | eqeq1 2741 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (𝑛 = 1 ↔ 𝑚 = 1)) |
| 121 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑚 → (𝑛 − 1) = (𝑚 − 1)) |
| 122 | 121 | eleq1d 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → ((𝑛 − 1) ∈ 𝐴 ↔ (𝑚 − 1) ∈ 𝐴)) |
| 123 | 122 | notbid 318 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (¬ (𝑛 − 1) ∈ 𝐴 ↔ ¬ (𝑚 − 1) ∈ 𝐴)) |
| 124 | 120, 123 | orbi12d 919 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ↔ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴))) |
| 125 | 121 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1))) |
| 126 | 124, 125 | ifbieq2d 4552 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1)))) |
| 127 | | simpl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → 𝑚 ∈ ℕ) |
| 128 | | iftrue 4531 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = ∅) |
| 129 | 128, 3 | eqeltrdi 2849 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) ∈ V) |
| 130 | 129 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) ∈ V) |
| 131 | 24, 126, 127, 130 | fvmptd3 7039 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1)))) |
| 132 | 128 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = ∅) |
| 133 | 131, 132 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = ∅) |
| 134 | 133 | ineq2d 4220 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ((𝐹‘𝑛) ∩ ∅)) |
| 135 | | in0 4395 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑛) ∩ ∅) = ∅ |
| 136 | 134, 135 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅) |
| 137 | 136 | adantll 714 |
. . . . . . . . 9
⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅) |
| 138 | 137 | ad5ant25 762 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅) |
| 139 | | fvex 6919 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺‘(𝑛 − 1)) ∈ V |
| 140 | 3, 139 | ifex 4576 |
. . . . . . . . . . . . . . 15
⊢ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ V |
| 141 | 140, 112 | mpan2 691 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝐹‘𝑛) = if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))) |
| 142 | 141, 9 | sylan9eq 2797 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ ¬
(𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = (𝐺‘(𝑛 − 1))) |
| 143 | 142 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬
(𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = (𝐺‘(𝑛 − 1))) |
| 144 | 143 | 3adant3 1133 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬
(𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = (𝐺‘(𝑛 − 1))) |
| 145 | 24 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ ∧ ¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))))) |
| 146 | 126 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ ℕ ∧ ¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) ∧ 𝑛 = 𝑚) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1)))) |
| 147 | | iffalse 4534 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = (𝐺‘(𝑚 − 1))) |
| 148 | 147 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ ℕ ∧ ¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) ∧ 𝑛 = 𝑚) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = (𝐺‘(𝑚 − 1))) |
| 149 | 146, 148 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ ℕ ∧ ¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) ∧ 𝑛 = 𝑚) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑚 − 1))) |
| 150 | | simpl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ ∧ ¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → 𝑚 ∈ ℕ) |
| 151 | | fvexd 6921 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ ∧ ¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑚 − 1)) ∈ V) |
| 152 | 145, 149,
150, 151 | fvmptd 7023 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ ¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = (𝐺‘(𝑚 − 1))) |
| 153 | 152 | adantll 714 |
. . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = (𝐺‘(𝑚 − 1))) |
| 154 | 153 | 3adant2 1132 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬
(𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = (𝐺‘(𝑚 − 1))) |
| 155 | 144, 154 | ineq12d 4221 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬
(𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1)))) |
| 156 | 155 | ad5ant245 1363 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1)))) |
| 157 | 16 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝑛 − 1) ∈ 𝐴) |
| 158 | | pm2.46 883 |
. . . . . . . . . . . . . . 15
⊢ (¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → ¬ ¬ (𝑚 − 1) ∈ 𝐴) |
| 159 | 158 | notnotrd 133 |
. . . . . . . . . . . . . 14
⊢ (¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → (𝑚 − 1) ∈ 𝐴) |
| 160 | 159 | adantl 481 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝑚 − 1) ∈ 𝐴) |
| 161 | | f1of1 6847 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺:𝐴–1-1-onto→𝑋 → 𝐺:𝐴–1-1→𝑋) |
| 162 | 11, 161 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺:𝐴–1-1→𝑋) |
| 163 | | dff14a 7290 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺:𝐴–1-1→𝑋 ↔ (𝐺:𝐴⟶𝑋 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))) |
| 164 | 162, 163 | sylib 218 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺:𝐴⟶𝑋 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))) |
| 165 | 164 | simprd 495 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))) |
| 166 | 165 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))) |
| 167 | 166 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))) |
| 168 | 157, 160,
167 | jca31 514 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (((𝑛 − 1) ∈ 𝐴 ∧ (𝑚 − 1) ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))) |
| 169 | | nncn 12274 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
| 170 | 169 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑛 ∈
ℂ) |
| 171 | 170 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 𝑛 ∈ ℂ) |
| 172 | | nncn 12274 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) |
| 173 | 172 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑚 ∈
ℂ) |
| 174 | 173 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 𝑚 ∈ ℂ) |
| 175 | | 1cnd 11256 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 1 ∈ ℂ) |
| 176 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 𝑛 ≠ 𝑚) |
| 177 | 171, 174,
175, 176 | subneintr2d 11666 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → (𝑛 − 1) ≠ (𝑚 − 1)) |
| 178 | 177 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝑛 − 1) ≠ (𝑚 − 1)) |
| 179 | | neeq1 3003 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑛 − 1) → (𝑥 ≠ 𝑦 ↔ (𝑛 − 1) ≠ 𝑦)) |
| 180 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑛 − 1) → (𝐺‘𝑥) = (𝐺‘(𝑛 − 1))) |
| 181 | 180 | neeq1d 3000 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑛 − 1) → ((𝐺‘𝑥) ≠ (𝐺‘𝑦) ↔ (𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦))) |
| 182 | 179, 181 | imbi12d 344 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑛 − 1) → ((𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)) ↔ ((𝑛 − 1) ≠ 𝑦 → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦)))) |
| 183 | | neeq2 3004 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑚 − 1) → ((𝑛 − 1) ≠ 𝑦 ↔ (𝑛 − 1) ≠ (𝑚 − 1))) |
| 184 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑚 − 1) → (𝐺‘𝑦) = (𝐺‘(𝑚 − 1))) |
| 185 | 184 | neeq2d 3001 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑚 − 1) → ((𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦) ↔ (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1)))) |
| 186 | 183, 185 | imbi12d 344 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑚 − 1) → (((𝑛 − 1) ≠ 𝑦 → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦)) ↔ ((𝑛 − 1) ≠ (𝑚 − 1) → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1))))) |
| 187 | 182, 186 | rspc2va 3634 |
. . . . . . . . . . . 12
⊢ ((((𝑛 − 1) ∈ 𝐴 ∧ (𝑚 − 1) ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))) → ((𝑛 − 1) ≠ (𝑚 − 1) → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1)))) |
| 188 | 168, 178,
187 | sylc 65 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1))) |
| 189 | 188 | neneqd 2945 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ¬ (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1))) |
| 190 | 18 | ad4ant13 751 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ 𝑋) |
| 191 | 13 | ffvelcdmda 7104 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 − 1) ∈ 𝐴) → (𝐺‘(𝑚 − 1)) ∈ 𝑋) |
| 192 | 159, 191 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑚 − 1)) ∈ 𝑋) |
| 193 | 192 | ad4ant14 752 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑚 − 1)) ∈ 𝑋) |
| 194 | | nnfoctbdjlem.dj |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Disj 𝑦 ∈ 𝑋 𝑦) |
| 195 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧) |
| 196 | 195 | disjor 5125 |
. . . . . . . . . . . . . 14
⊢
(Disj 𝑦
∈ 𝑋 𝑦 ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅)) |
| 197 | 194, 196 | sylib 218 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅)) |
| 198 | 197 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅)) |
| 199 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → (𝑦 = 𝑧 ↔ (𝐺‘(𝑛 − 1)) = 𝑧)) |
| 200 | | ineq1 4213 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → (𝑦 ∩ 𝑧) = ((𝐺‘(𝑛 − 1)) ∩ 𝑧)) |
| 201 | 200 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → ((𝑦 ∩ 𝑧) = ∅ ↔ ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅)) |
| 202 | 199, 201 | orbi12d 919 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → ((𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅) ↔ ((𝐺‘(𝑛 − 1)) = 𝑧 ∨ ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅))) |
| 203 | | eqeq2 2749 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → ((𝐺‘(𝑛 − 1)) = 𝑧 ↔ (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)))) |
| 204 | | ineq2 4214 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1)))) |
| 205 | 204 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → (((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅ ↔ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅)) |
| 206 | 203, 205 | orbi12d 919 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → (((𝐺‘(𝑛 − 1)) = 𝑧 ∨ ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅) ↔ ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅))) |
| 207 | 202, 206 | rspc2va 3634 |
. . . . . . . . . . . 12
⊢ ((((𝐺‘(𝑛 − 1)) ∈ 𝑋 ∧ (𝐺‘(𝑚 − 1)) ∈ 𝑋) ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅)) → ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅)) |
| 208 | 190, 193,
198, 207 | syl21anc 838 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅)) |
| 209 | 208 | adantllr 719 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅)) |
| 210 | | orel1 889 |
. . . . . . . . . 10
⊢ (¬
(𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) → (((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅) → ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅)) |
| 211 | 189, 209,
210 | sylc 65 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅) |
| 212 | 156, 211 | eqtrd 2777 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅) |
| 213 | 138, 212 | pm2.61dan 813 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅) |
| 214 | 119, 213 | pm2.61dan 813 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅) |
| 215 | 214 | olcd 875 |
. . . . 5
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)) |
| 216 | 110, 215 | pm2.61dane 3029 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) → (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)) |
| 217 | 216 | ralrimivva 3202 |
. . 3
⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑚 ∈ ℕ (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)) |
| 218 | | fveq2 6906 |
. . . 4
⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚)) |
| 219 | 218 | disjor 5125 |
. . 3
⊢
(Disj 𝑛
∈ ℕ (𝐹‘𝑛) ↔ ∀𝑛 ∈ ℕ ∀𝑚 ∈ ℕ (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)) |
| 220 | 217, 219 | sylibr 234 |
. 2
⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐹‘𝑛)) |
| 221 | | nnex 12272 |
. . . . 5
⊢ ℕ
∈ V |
| 222 | 221 | mptex 7243 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦
if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))) ∈ V |
| 223 | 24, 222 | eqeltri 2837 |
. . 3
⊢ 𝐹 ∈ V |
| 224 | | foeq1 6816 |
. . . 4
⊢ (𝑓 = 𝐹 → (𝑓:ℕ–onto→(𝑋 ∪ {∅}) ↔ 𝐹:ℕ–onto→(𝑋 ∪ {∅}))) |
| 225 | | simpl 482 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑛 ∈ ℕ) → 𝑓 = 𝐹) |
| 226 | 225 | fveq1d 6908 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) = (𝐹‘𝑛)) |
| 227 | 226 | disjeq2dv 5115 |
. . . 4
⊢ (𝑓 = 𝐹 → (Disj 𝑛 ∈ ℕ (𝑓‘𝑛) ↔ Disj 𝑛 ∈ ℕ (𝐹‘𝑛))) |
| 228 | 224, 227 | anbi12d 632 |
. . 3
⊢ (𝑓 = 𝐹 → ((𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) ↔ (𝐹:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝐹‘𝑛)))) |
| 229 | 223, 228 | spcev 3606 |
. 2
⊢ ((𝐹:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝐹‘𝑛)) → ∃𝑓(𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛))) |
| 230 | 109, 220,
229 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑓(𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛))) |