Step | Hyp | Ref
| Expression |
1 | | iftrue 4465 |
. . . . . . . 8
⊢ ((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = ∅) |
2 | 1 | adantl 482 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = ∅) |
3 | | 0ex 5229 |
. . . . . . . . 9
⊢ ∅
∈ V |
4 | 3 | snid 4597 |
. . . . . . . 8
⊢ ∅
∈ {∅} |
5 | | elun2 4110 |
. . . . . . . 8
⊢ (∅
∈ {∅} → ∅ ∈ (𝑋 ∪ {∅})) |
6 | 4, 5 | ax-mp 5 |
. . . . . . 7
⊢ ∅
∈ (𝑋 ∪
{∅}) |
7 | 2, 6 | eqeltrdi 2847 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅})) |
8 | 7 | adantll 711 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅})) |
9 | | iffalse 4468 |
. . . . . . 7
⊢ (¬
(𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑛 − 1))) |
10 | 9 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑛 − 1))) |
11 | | nnfoctbdjlem.g |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺:𝐴–1-1-onto→𝑋) |
12 | | f1of 6708 |
. . . . . . . . . . 11
⊢ (𝐺:𝐴–1-1-onto→𝑋 → 𝐺:𝐴⟶𝑋) |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:𝐴⟶𝑋) |
14 | 13 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → 𝐺:𝐴⟶𝑋) |
15 | | pm2.46 880 |
. . . . . . . . . . 11
⊢ (¬
(𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → ¬ ¬ (𝑛 − 1) ∈ 𝐴) |
16 | 15 | notnotrd 133 |
. . . . . . . . . 10
⊢ (¬
(𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) → (𝑛 − 1) ∈ 𝐴) |
17 | 16 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝑛 − 1) ∈ 𝐴) |
18 | 14, 17 | ffvelrnd 6954 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ 𝑋) |
19 | 18 | adantlr 712 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ 𝑋) |
20 | | elun1 4109 |
. . . . . . 7
⊢ ((𝐺‘(𝑛 − 1)) ∈ 𝑋 → (𝐺‘(𝑛 − 1)) ∈ (𝑋 ∪ {∅})) |
21 | 19, 20 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ (𝑋 ∪ {∅})) |
22 | 10, 21 | eqeltrd 2839 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅})) |
23 | 8, 22 | pm2.61dan 810 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ (𝑋 ∪ {∅})) |
24 | | nnfoctbdjlem.f |
. . . 4
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))) |
25 | 23, 24 | fmptd 6980 |
. . 3
⊢ (𝜑 → 𝐹:ℕ⟶(𝑋 ∪ {∅})) |
26 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
27 | | f1ofo 6715 |
. . . . . . . . . . . . 13
⊢ (𝐺:𝐴–1-1-onto→𝑋 → 𝐺:𝐴–onto→𝑋) |
28 | | forn 6683 |
. . . . . . . . . . . . 13
⊢ (𝐺:𝐴–onto→𝑋 → ran 𝐺 = 𝑋) |
29 | 11, 27, 28 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝐺 = 𝑋) |
30 | 29 | eqcomd 2744 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 = ran 𝐺) |
31 | 30 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑋 = ran 𝐺) |
32 | 26, 31 | eleqtrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ ran 𝐺) |
33 | 13 | ffnd 6593 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 Fn 𝐴) |
34 | | fvelrnb 6822 |
. . . . . . . . . . 11
⊢ (𝐺 Fn 𝐴 → (𝑦 ∈ ran 𝐺 ↔ ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦)) |
35 | 33, 34 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ ran 𝐺 ↔ ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦)) |
36 | 35 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑦 ∈ ran 𝐺 ↔ ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦)) |
37 | 32, 36 | mpbid 231 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦) |
38 | | nnfoctbdjlem.a |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ⊆ ℕ) |
39 | 38 | sselda 3920 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℕ) |
40 | 39 | peano2nnd 12000 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑘 + 1) ∈ ℕ) |
41 | 40 | 3adant3 1131 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝑘 + 1) ∈ ℕ) |
42 | 24 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))))) |
43 | | 1red 10986 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 1 ∈
ℝ) |
44 | | 1red 10986 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℝ) |
45 | 39 | nnrpd 12780 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℝ+) |
46 | 44, 45 | ltaddrp2d 12816 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 < (𝑘 + 1)) |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 1 < (𝑘 + 1)) |
48 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = (𝑘 + 1) → 𝑛 = (𝑘 + 1)) |
49 | 48 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = (𝑘 + 1) → (𝑘 + 1) = 𝑛) |
50 | 49 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝑘 + 1) = 𝑛) |
51 | 47, 50 | breqtrd 5099 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 1 < 𝑛) |
52 | 43, 51 | gtned 11120 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 𝑛 ≠ 1) |
53 | 52 | neneqd 2948 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → ¬ 𝑛 = 1) |
54 | | oveq1 7274 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = (𝑘 + 1) → (𝑛 − 1) = ((𝑘 + 1) − 1)) |
55 | 39 | nncnd 11999 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℂ) |
56 | | 1cnd 10980 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℂ) |
57 | 55, 56 | pncand 11343 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 + 1) − 1) = 𝑘) |
58 | 54, 57 | sylan9eqr 2800 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝑛 − 1) = 𝑘) |
59 | | simplr 766 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → 𝑘 ∈ 𝐴) |
60 | 58, 59 | eqeltrd 2839 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝑛 − 1) ∈ 𝐴) |
61 | 60 | notnotd 144 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → ¬ ¬ (𝑛 − 1) ∈ 𝐴) |
62 | | ioran 981 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
(𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ↔ (¬ 𝑛 = 1 ∧ ¬ ¬ (𝑛 − 1) ∈ 𝐴)) |
63 | 53, 61, 62 | sylanbrc 583 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) |
64 | 63 | iffalsed 4470 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑛 − 1))) |
65 | 58 | fveq2d 6770 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → (𝐺‘(𝑛 − 1)) = (𝐺‘𝑘)) |
66 | 64, 65 | eqtrd 2778 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑛 = (𝑘 + 1)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘𝑘)) |
67 | 13 | ffvelrnda 6953 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘𝑘) ∈ 𝑋) |
68 | 42, 66, 40, 67 | fvmptd 6874 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘(𝑘 + 1)) = (𝐺‘𝑘)) |
69 | 68 | 3adant3 1131 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝐹‘(𝑘 + 1)) = (𝐺‘𝑘)) |
70 | | simp3 1137 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝐺‘𝑘) = 𝑦) |
71 | 69, 70 | eqtrd 2778 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → (𝐹‘(𝑘 + 1)) = 𝑦) |
72 | | fveq2 6766 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑘 + 1) → (𝐹‘𝑚) = (𝐹‘(𝑘 + 1))) |
73 | 72 | eqeq1d 2740 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑘 + 1) → ((𝐹‘𝑚) = 𝑦 ↔ (𝐹‘(𝑘 + 1)) = 𝑦)) |
74 | 73 | rspcev 3559 |
. . . . . . . . . . . 12
⊢ (((𝑘 + 1) ∈ ℕ ∧
(𝐹‘(𝑘 + 1)) = 𝑦) → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦) |
75 | 41, 71, 74 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ (𝐺‘𝑘) = 𝑦) → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦) |
76 | 75 | 3exp 1118 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ 𝐴 → ((𝐺‘𝑘) = 𝑦 → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦))) |
77 | 76 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑘 ∈ 𝐴 → ((𝐺‘𝑘) = 𝑦 → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦))) |
78 | 77 | rexlimdv 3210 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑘 ∈ 𝐴 (𝐺‘𝑘) = 𝑦 → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦)) |
79 | 37, 78 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦) |
80 | | id 22 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑚) = 𝑦 → (𝐹‘𝑚) = 𝑦) |
81 | 80 | eqcomd 2744 |
. . . . . . . . 9
⊢ ((𝐹‘𝑚) = 𝑦 → 𝑦 = (𝐹‘𝑚)) |
82 | 81 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑚 ∈ ℕ) → ((𝐹‘𝑚) = 𝑦 → 𝑦 = (𝐹‘𝑚))) |
83 | 82 | reximdva 3201 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∃𝑚 ∈ ℕ (𝐹‘𝑚) = 𝑦 → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))) |
84 | 79, 83 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)) |
85 | 84 | adantlr 712 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)) |
86 | | simpll 764 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ ¬ 𝑦 ∈ 𝑋) → 𝜑) |
87 | | elunnel1 4083 |
. . . . . . . 8
⊢ ((𝑦 ∈ (𝑋 ∪ {∅}) ∧ ¬ 𝑦 ∈ 𝑋) → 𝑦 ∈ {∅}) |
88 | | elsni 4578 |
. . . . . . . 8
⊢ (𝑦 ∈ {∅} → 𝑦 = ∅) |
89 | 87, 88 | syl 17 |
. . . . . . 7
⊢ ((𝑦 ∈ (𝑋 ∪ {∅}) ∧ ¬ 𝑦 ∈ 𝑋) → 𝑦 = ∅) |
90 | 89 | adantll 711 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ ¬ 𝑦 ∈ 𝑋) → 𝑦 = ∅) |
91 | | 1nn 11994 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
92 | 91 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = ∅) → 1 ∈
ℕ) |
93 | 1 | orcs 872 |
. . . . . . . . . 10
⊢ (𝑛 = 1 → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = ∅) |
94 | 91 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℕ) |
95 | 3 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ∅ ∈
V) |
96 | 24, 93, 94, 95 | fvmptd3 6890 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘1) = ∅) |
97 | 96 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = ∅) → (𝐹‘1) = ∅) |
98 | | id 22 |
. . . . . . . . . 10
⊢ (𝑦 = ∅ → 𝑦 = ∅) |
99 | 98 | eqcomd 2744 |
. . . . . . . . 9
⊢ (𝑦 = ∅ → ∅ =
𝑦) |
100 | 99 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = ∅) → ∅ = 𝑦) |
101 | 97, 100 | eqtr2d 2779 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = ∅) → 𝑦 = (𝐹‘1)) |
102 | | fveq2 6766 |
. . . . . . . 8
⊢ (𝑚 = 1 → (𝐹‘𝑚) = (𝐹‘1)) |
103 | 102 | rspceeqv 3574 |
. . . . . . 7
⊢ ((1
∈ ℕ ∧ 𝑦 =
(𝐹‘1)) →
∃𝑚 ∈ ℕ
𝑦 = (𝐹‘𝑚)) |
104 | 92, 101, 103 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = ∅) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)) |
105 | 86, 90, 104 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) ∧ ¬ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)) |
106 | 85, 105 | pm2.61dan 810 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∪ {∅})) → ∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)) |
107 | 106 | ralrimiva 3108 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ (𝑋 ∪ {∅})∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚)) |
108 | | dffo3 6970 |
. . 3
⊢ (𝐹:ℕ–onto→(𝑋 ∪ {∅}) ↔ (𝐹:ℕ⟶(𝑋 ∪ {∅}) ∧ ∀𝑦 ∈ (𝑋 ∪ {∅})∃𝑚 ∈ ℕ 𝑦 = (𝐹‘𝑚))) |
109 | 25, 107, 108 | sylanbrc 583 |
. 2
⊢ (𝜑 → 𝐹:ℕ–onto→(𝑋 ∪ {∅})) |
110 | | animorrl 978 |
. . . . 5
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 = 𝑚) → (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)) |
111 | 2, 3 | eqeltrdi 2847 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ V) |
112 | 24 | fvmpt2 6878 |
. . . . . . . . . . . . 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 2778 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = ∅) |
115 | 114 | ineq1d 4145 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = (∅ ∩ (𝐹‘𝑚))) |
116 | | 0in 4327 |
. . . . . . . . . 10
⊢ (∅
∩ (𝐹‘𝑚)) = ∅ |
117 | 115, 116 | eqtrdi 2794 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅) |
118 | 117 | adantlr 712 |
. . . . . . . 8
⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅) |
119 | 118 | ad4ant24 751 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅) |
120 | | eqeq1 2742 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (𝑛 = 1 ↔ 𝑚 = 1)) |
121 | | oveq1 7274 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑚 → (𝑛 − 1) = (𝑚 − 1)) |
122 | 121 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → ((𝑛 − 1) ∈ 𝐴 ↔ (𝑚 − 1) ∈ 𝐴)) |
123 | 122 | notbid 318 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (¬ (𝑛 − 1) ∈ 𝐴 ↔ ¬ (𝑚 − 1) ∈ 𝐴)) |
124 | 120, 123 | orbi12d 916 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ↔ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴))) |
125 | 121 | fveq2d 6770 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1))) |
126 | 124, 125 | ifbieq2d 4485 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1)))) |
127 | | simpl 483 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → 𝑚 ∈ ℕ) |
128 | | iftrue 4465 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = ∅) |
129 | 128, 3 | eqeltrdi 2847 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) ∈ V) |
130 | 129 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) ∈ V) |
131 | 24, 126, 127, 130 | fvmptd3 6890 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1)))) |
132 | 128 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = ∅) |
133 | 131, 132 | eqtrd 2778 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = ∅) |
134 | 133 | ineq2d 4146 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ((𝐹‘𝑛) ∩ ∅)) |
135 | | in0 4325 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑛) ∩ ∅) = ∅ |
136 | 134, 135 | eqtrdi 2794 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅) |
137 | 136 | adantll 711 |
. . . . . . . . 9
⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅) |
138 | 137 | ad5ant25 759 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅) |
139 | | fvex 6779 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺‘(𝑛 − 1)) ∈ V |
140 | 3, 139 | ifex 4509 |
. . . . . . . . . . . . . . 15
⊢ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) ∈ V |
141 | 140, 112 | mpan2 688 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝐹‘𝑛) = if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))) |
142 | 141, 9 | sylan9eq 2798 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ ¬
(𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = (𝐺‘(𝑛 − 1))) |
143 | 142 | adantlr 712 |
. . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬
(𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = (𝐺‘(𝑛 − 1))) |
144 | 143 | 3adant3 1131 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬
(𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑛) = (𝐺‘(𝑛 − 1))) |
145 | 24 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ ∧ ¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))))) |
146 | 126 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ ℕ ∧ ¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) ∧ 𝑛 = 𝑚) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1)))) |
147 | | iffalse 4468 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = (𝐺‘(𝑚 − 1))) |
148 | 147 | ad2antlr 724 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ ℕ ∧ ¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) ∧ 𝑛 = 𝑚) → if((𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑚 − 1))) = (𝐺‘(𝑚 − 1))) |
149 | 146, 148 | eqtrd 2778 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ ℕ ∧ ¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) ∧ 𝑛 = 𝑚) → if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))) = (𝐺‘(𝑚 − 1))) |
150 | | simpl 483 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ ∧ ¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → 𝑚 ∈ ℕ) |
151 | | fvexd 6781 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ ∧ ¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑚 − 1)) ∈ V) |
152 | 145, 149,
150, 151 | fvmptd 6874 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ ¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = (𝐺‘(𝑚 − 1))) |
153 | 152 | adantll 711 |
. . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = (𝐺‘(𝑚 − 1))) |
154 | 153 | 3adant2 1130 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬
(𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐹‘𝑚) = (𝐺‘(𝑚 − 1))) |
155 | 144, 154 | ineq12d 4147 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ ¬
(𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1)))) |
156 | 155 | ad5ant245 1360 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1)))) |
157 | 16 | ad2antlr 724 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝑛 − 1) ∈ 𝐴) |
158 | | pm2.46 880 |
. . . . . . . . . . . . . . 15
⊢ (¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → ¬ ¬ (𝑚 − 1) ∈ 𝐴) |
159 | 158 | notnotrd 133 |
. . . . . . . . . . . . . 14
⊢ (¬
(𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴) → (𝑚 − 1) ∈ 𝐴) |
160 | 159 | adantl 482 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝑚 − 1) ∈ 𝐴) |
161 | | f1of1 6707 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺:𝐴–1-1-onto→𝑋 → 𝐺:𝐴–1-1→𝑋) |
162 | 11, 161 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺:𝐴–1-1→𝑋) |
163 | | dff14a 7135 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺:𝐴–1-1→𝑋 ↔ (𝐺:𝐴⟶𝑋 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))) |
164 | 162, 163 | sylib 217 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺:𝐴⟶𝑋 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))) |
165 | 164 | simprd 496 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))) |
166 | 165 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))) |
167 | 166 | ad3antrrr 727 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))) |
168 | 157, 160,
167 | jca31 515 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (((𝑛 − 1) ∈ 𝐴 ∧ (𝑚 − 1) ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)))) |
169 | | nncn 11991 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
170 | 169 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑛 ∈
ℂ) |
171 | 170 | ad2antlr 724 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 𝑛 ∈ ℂ) |
172 | | nncn 11991 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) |
173 | 172 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑚 ∈
ℂ) |
174 | 173 | ad2antlr 724 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 𝑚 ∈ ℂ) |
175 | | 1cnd 10980 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 1 ∈ ℂ) |
176 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → 𝑛 ≠ 𝑚) |
177 | 171, 174,
175, 176 | subneintr2d 11388 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → (𝑛 − 1) ≠ (𝑚 − 1)) |
178 | 177 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝑛 − 1) ≠ (𝑚 − 1)) |
179 | | neeq1 3006 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑛 − 1) → (𝑥 ≠ 𝑦 ↔ (𝑛 − 1) ≠ 𝑦)) |
180 | | fveq2 6766 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑛 − 1) → (𝐺‘𝑥) = (𝐺‘(𝑛 − 1))) |
181 | 180 | neeq1d 3003 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑛 − 1) → ((𝐺‘𝑥) ≠ (𝐺‘𝑦) ↔ (𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦))) |
182 | 179, 181 | imbi12d 345 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑛 − 1) → ((𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦)) ↔ ((𝑛 − 1) ≠ 𝑦 → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦)))) |
183 | | neeq2 3007 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑚 − 1) → ((𝑛 − 1) ≠ 𝑦 ↔ (𝑛 − 1) ≠ (𝑚 − 1))) |
184 | | fveq2 6766 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑚 − 1) → (𝐺‘𝑦) = (𝐺‘(𝑚 − 1))) |
185 | 184 | neeq2d 3004 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑚 − 1) → ((𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦) ↔ (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1)))) |
186 | 183, 185 | imbi12d 345 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑚 − 1) → (((𝑛 − 1) ≠ 𝑦 → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘𝑦)) ↔ ((𝑛 − 1) ≠ (𝑚 − 1) → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1))))) |
187 | 182, 186 | rspc2va 3570 |
. . . . . . . . . . . 12
⊢ ((((𝑛 − 1) ∈ 𝐴 ∧ (𝑚 − 1) ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐺‘𝑥) ≠ (𝐺‘𝑦))) → ((𝑛 − 1) ≠ (𝑚 − 1) → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1)))) |
188 | 168, 178,
187 | sylc 65 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ≠ (𝐺‘(𝑚 − 1))) |
189 | 188 | neneqd 2948 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ¬ (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1))) |
190 | 18 | ad4ant13 748 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑛 − 1)) ∈ 𝑋) |
191 | 13 | ffvelrnda 6953 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 − 1) ∈ 𝐴) → (𝐺‘(𝑚 − 1)) ∈ 𝑋) |
192 | 159, 191 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑚 − 1)) ∈ 𝑋) |
193 | 192 | ad4ant14 749 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → (𝐺‘(𝑚 − 1)) ∈ 𝑋) |
194 | | nnfoctbdjlem.dj |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Disj 𝑦 ∈ 𝑋 𝑦) |
195 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧) |
196 | 195 | disjor 5053 |
. . . . . . . . . . . . . 14
⊢
(Disj 𝑦
∈ 𝑋 𝑦 ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅)) |
197 | 194, 196 | sylib 217 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅)) |
198 | 197 | ad3antrrr 727 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅)) |
199 | | eqeq1 2742 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → (𝑦 = 𝑧 ↔ (𝐺‘(𝑛 − 1)) = 𝑧)) |
200 | | ineq1 4139 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → (𝑦 ∩ 𝑧) = ((𝐺‘(𝑛 − 1)) ∩ 𝑧)) |
201 | 200 | eqeq1d 2740 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → ((𝑦 ∩ 𝑧) = ∅ ↔ ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅)) |
202 | 199, 201 | orbi12d 916 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝐺‘(𝑛 − 1)) → ((𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅) ↔ ((𝐺‘(𝑛 − 1)) = 𝑧 ∨ ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅))) |
203 | | eqeq2 2750 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → ((𝐺‘(𝑛 − 1)) = 𝑧 ↔ (𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)))) |
204 | | ineq2 4140 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1)))) |
205 | 204 | eqeq1d 2740 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → (((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅ ↔ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅)) |
206 | 203, 205 | orbi12d 916 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝐺‘(𝑚 − 1)) → (((𝐺‘(𝑛 − 1)) = 𝑧 ∨ ((𝐺‘(𝑛 − 1)) ∩ 𝑧) = ∅) ↔ ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅))) |
207 | 202, 206 | rspc2va 3570 |
. . . . . . . . . . . 12
⊢ ((((𝐺‘(𝑛 − 1)) ∈ 𝑋 ∧ (𝐺‘(𝑚 − 1)) ∈ 𝑋) ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦 = 𝑧 ∨ (𝑦 ∩ 𝑧) = ∅)) → ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅)) |
208 | 190, 193,
198, 207 | syl21anc 835 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅)) |
209 | 208 | adantllr 716 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐺‘(𝑛 − 1)) = (𝐺‘(𝑚 − 1)) ∨ ((𝐺‘(𝑛 − 1)) ∩ (𝐺‘(𝑚 − 1))) = ∅)) |
210 | | orel1 886 |
. . . . . . . . . 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 2778 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) ∧ ¬ (𝑚 = 1 ∨ ¬ (𝑚 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅) |
213 | 138, 212 | pm2.61dan 810 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) ∧ ¬ (𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴)) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅) |
214 | 119, 213 | pm2.61dan 810 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅) |
215 | 214 | olcd 871 |
. . . . 5
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) ∧ 𝑛 ≠ 𝑚) → (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)) |
216 | 110, 215 | pm2.61dane 3032 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ)) → (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)) |
217 | 216 | ralrimivva 3115 |
. . 3
⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑚 ∈ ℕ (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)) |
218 | | fveq2 6766 |
. . . 4
⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚)) |
219 | 218 | disjor 5053 |
. . 3
⊢
(Disj 𝑛
∈ ℕ (𝐹‘𝑛) ↔ ∀𝑛 ∈ ℕ ∀𝑚 ∈ ℕ (𝑛 = 𝑚 ∨ ((𝐹‘𝑛) ∩ (𝐹‘𝑚)) = ∅)) |
220 | 217, 219 | sylibr 233 |
. 2
⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐹‘𝑛)) |
221 | | nnex 11989 |
. . . . 5
⊢ ℕ
∈ V |
222 | 221 | mptex 7091 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦
if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))) ∈ V |
223 | 24, 222 | eqeltri 2835 |
. . 3
⊢ 𝐹 ∈ V |
224 | | foeq1 6676 |
. . . 4
⊢ (𝑓 = 𝐹 → (𝑓:ℕ–onto→(𝑋 ∪ {∅}) ↔ 𝐹:ℕ–onto→(𝑋 ∪ {∅}))) |
225 | | simpl 483 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑛 ∈ ℕ) → 𝑓 = 𝐹) |
226 | 225 | fveq1d 6768 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) = (𝐹‘𝑛)) |
227 | 226 | disjeq2dv 5043 |
. . . 4
⊢ (𝑓 = 𝐹 → (Disj 𝑛 ∈ ℕ (𝑓‘𝑛) ↔ Disj 𝑛 ∈ ℕ (𝐹‘𝑛))) |
228 | 224, 227 | anbi12d 631 |
. . 3
⊢ (𝑓 = 𝐹 → ((𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) ↔ (𝐹:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝐹‘𝑛)))) |
229 | 223, 228 | spcev 3542 |
. 2
⊢ ((𝐹:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝐹‘𝑛)) → ∃𝑓(𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛))) |
230 | 109, 220,
229 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑓(𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛))) |