Step | Hyp | Ref
| Expression |
1 | | preq2 4738 |
. . . . . 6
⊢ (𝑧 = (𝐹‘𝐵) → {0, 𝑧} = {0, (𝐹‘𝐵)}) |
2 | 1 | eqeq2d 2745 |
. . . . 5
⊢ (𝑧 = (𝐹‘𝐵) → ((𝐹 “ {𝑋, 𝐵}) = {0, 𝑧} ↔ (𝐹 “ {𝑋, 𝐵}) = {0, (𝐹‘𝐵)})) |
3 | | f1of 6848 |
. . . . . . . . 9
⊢ (𝐹:𝐶–1-1-onto→𝑊 → 𝐹:𝐶⟶𝑊) |
4 | 3 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) → 𝐹:𝐶⟶𝑊) |
5 | 4 | adantr 480 |
. . . . . . 7
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → 𝐹:𝐶⟶𝑊) |
6 | | simpr3 1195 |
. . . . . . 7
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → 𝐵 ∈ 𝐶) |
7 | 5, 6 | ffvelcdmd 7104 |
. . . . . 6
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → (𝐹‘𝐵) ∈ 𝑊) |
8 | | isubgr3stgr.w |
. . . . . . . . . 10
⊢ 𝑊 = (Vtx‘𝑆) |
9 | | isubgr3stgr.s |
. . . . . . . . . . 11
⊢ 𝑆 = (StarGr‘𝑁) |
10 | 9 | fveq2i 6909 |
. . . . . . . . . 10
⊢
(Vtx‘𝑆) =
(Vtx‘(StarGr‘𝑁)) |
11 | | isubgr3stgr.n |
. . . . . . . . . . 11
⊢ 𝑁 ∈
ℕ0 |
12 | | stgrvtx 47856 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (Vtx‘(StarGr‘𝑁)) = (0...𝑁)) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . . 10
⊢
(Vtx‘(StarGr‘𝑁)) = (0...𝑁) |
14 | 8, 10, 13 | 3eqtri 2766 |
. . . . . . . . 9
⊢ 𝑊 = (0...𝑁) |
15 | 14 | eleq2i 2830 |
. . . . . . . 8
⊢ ((𝐹‘𝐵) ∈ 𝑊 ↔ (𝐹‘𝐵) ∈ (0...𝑁)) |
16 | | fz0sn0fz1 13681 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (0...𝑁) = ({0} ∪
(1...𝑁))) |
17 | 11, 16 | ax-mp 5 |
. . . . . . . . 9
⊢
(0...𝑁) = ({0} ∪
(1...𝑁)) |
18 | 17 | eleq2i 2830 |
. . . . . . . 8
⊢ ((𝐹‘𝐵) ∈ (0...𝑁) ↔ (𝐹‘𝐵) ∈ ({0} ∪ (1...𝑁))) |
19 | | elun 4162 |
. . . . . . . . 9
⊢ ((𝐹‘𝐵) ∈ ({0} ∪ (1...𝑁)) ↔ ((𝐹‘𝐵) ∈ {0} ∨ (𝐹‘𝐵) ∈ (1...𝑁))) |
20 | | fvex 6919 |
. . . . . . . . . . 11
⊢ (𝐹‘𝐵) ∈ V |
21 | 20 | elsn 4645 |
. . . . . . . . . 10
⊢ ((𝐹‘𝐵) ∈ {0} ↔ (𝐹‘𝐵) = 0) |
22 | 21 | orbi1i 913 |
. . . . . . . . 9
⊢ (((𝐹‘𝐵) ∈ {0} ∨ (𝐹‘𝐵) ∈ (1...𝑁)) ↔ ((𝐹‘𝐵) = 0 ∨ (𝐹‘𝐵) ∈ (1...𝑁))) |
23 | 19, 22 | bitri 275 |
. . . . . . . 8
⊢ ((𝐹‘𝐵) ∈ ({0} ∪ (1...𝑁)) ↔ ((𝐹‘𝐵) = 0 ∨ (𝐹‘𝐵) ∈ (1...𝑁))) |
24 | 15, 18, 23 | 3bitri 297 |
. . . . . . 7
⊢ ((𝐹‘𝐵) ∈ 𝑊 ↔ ((𝐹‘𝐵) = 0 ∨ (𝐹‘𝐵) ∈ (1...𝑁))) |
25 | | eqeq2 2746 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑋) = 0 → ((𝐹‘𝐵) = (𝐹‘𝑋) ↔ (𝐹‘𝐵) = 0)) |
26 | 25 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) → ((𝐹‘𝐵) = (𝐹‘𝑋) ↔ (𝐹‘𝐵) = 0)) |
27 | 26 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ((𝐹‘𝐵) = (𝐹‘𝑋) ↔ (𝐹‘𝐵) = 0)) |
28 | | f1of1 6847 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐶–1-1-onto→𝑊 → 𝐹:𝐶–1-1→𝑊) |
29 | | dff14a 7289 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝐶–1-1→𝑊 ↔ (𝐹:𝐶⟶𝑊 ∧ ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐶 (𝑎 ≠ 𝑏 → (𝐹‘𝑎) ≠ (𝐹‘𝑏)))) |
30 | | simpl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝐵) → 𝑎 = 𝑋) |
31 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
32 | 30, 31 | neeq12d 2999 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝐵) → (𝑎 ≠ 𝑏 ↔ 𝑋 ≠ 𝐵)) |
33 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝑋 → (𝐹‘𝑎) = (𝐹‘𝑋)) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝐵) → (𝐹‘𝑎) = (𝐹‘𝑋)) |
35 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = 𝐵 → (𝐹‘𝑏) = (𝐹‘𝐵)) |
36 | 35 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝐵) → (𝐹‘𝑏) = (𝐹‘𝐵)) |
37 | 34, 36 | neeq12d 2999 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝐵) → ((𝐹‘𝑎) ≠ (𝐹‘𝑏) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝐵))) |
38 | 32, 37 | imbi12d 344 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝐵) → ((𝑎 ≠ 𝑏 → (𝐹‘𝑎) ≠ (𝐹‘𝑏)) ↔ (𝑋 ≠ 𝐵 → (𝐹‘𝑋) ≠ (𝐹‘𝐵)))) |
39 | 38 | rspc2gv 3631 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐶 (𝑎 ≠ 𝑏 → (𝐹‘𝑎) ≠ (𝐹‘𝑏)) → (𝑋 ≠ 𝐵 → (𝐹‘𝑋) ≠ (𝐹‘𝐵)))) |
40 | 39 | 3adant1 1129 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐶 (𝑎 ≠ 𝑏 → (𝐹‘𝑎) ≠ (𝐹‘𝑏)) → (𝑋 ≠ 𝐵 → (𝐹‘𝑋) ≠ (𝐹‘𝐵)))) |
41 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ≠ 𝐵 → (𝐹‘𝑋) ≠ (𝐹‘𝐵)) → (𝑋 ≠ 𝐵 → (𝐹‘𝑋) ≠ (𝐹‘𝐵))) |
42 | | eqneqall 2948 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑋) = (𝐹‘𝐵) → ((𝐹‘𝑋) ≠ (𝐹‘𝐵) → (𝐹‘𝐵) ∈ (1...𝑁))) |
43 | 42 | eqcoms 2742 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝐵) = (𝐹‘𝑋) → ((𝐹‘𝑋) ≠ (𝐹‘𝐵) → (𝐹‘𝐵) ∈ (1...𝑁))) |
44 | 43 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑋) ≠ (𝐹‘𝐵) → ((𝐹‘𝐵) = (𝐹‘𝑋) → (𝐹‘𝐵) ∈ (1...𝑁))) |
45 | 41, 44 | syl6com 37 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ≠ 𝐵 → ((𝑋 ≠ 𝐵 → (𝐹‘𝑋) ≠ (𝐹‘𝐵)) → ((𝐹‘𝐵) = (𝐹‘𝑋) → (𝐹‘𝐵) ∈ (1...𝑁)))) |
46 | 45 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝑋 ≠ 𝐵 → (𝐹‘𝑋) ≠ (𝐹‘𝐵)) → ((𝐹‘𝐵) = (𝐹‘𝑋) → (𝐹‘𝐵) ∈ (1...𝑁)))) |
47 | 40, 46 | syld 47 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐶 (𝑎 ≠ 𝑏 → (𝐹‘𝑎) ≠ (𝐹‘𝑏)) → ((𝐹‘𝐵) = (𝐹‘𝑋) → (𝐹‘𝐵) ∈ (1...𝑁)))) |
48 | 47 | adantld 490 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐹:𝐶⟶𝑊 ∧ ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐶 (𝑎 ≠ 𝑏 → (𝐹‘𝑎) ≠ (𝐹‘𝑏))) → ((𝐹‘𝐵) = (𝐹‘𝑋) → (𝐹‘𝐵) ∈ (1...𝑁)))) |
49 | 29, 48 | biimtrid 242 |
. . . . . . . . . . . 12
⊢ ((𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐹:𝐶–1-1→𝑊 → ((𝐹‘𝐵) = (𝐹‘𝑋) → (𝐹‘𝐵) ∈ (1...𝑁)))) |
50 | 28, 49 | syl5com 31 |
. . . . . . . . . . 11
⊢ (𝐹:𝐶–1-1-onto→𝑊 → ((𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐹‘𝐵) = (𝐹‘𝑋) → (𝐹‘𝐵) ∈ (1...𝑁)))) |
51 | 50 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) → ((𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐹‘𝐵) = (𝐹‘𝑋) → (𝐹‘𝐵) ∈ (1...𝑁)))) |
52 | 51 | imp 406 |
. . . . . . . . 9
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ((𝐹‘𝐵) = (𝐹‘𝑋) → (𝐹‘𝐵) ∈ (1...𝑁))) |
53 | 27, 52 | sylbird 260 |
. . . . . . . 8
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ((𝐹‘𝐵) = 0 → (𝐹‘𝐵) ∈ (1...𝑁))) |
54 | | idd 24 |
. . . . . . . 8
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ((𝐹‘𝐵) ∈ (1...𝑁) → (𝐹‘𝐵) ∈ (1...𝑁))) |
55 | 53, 54 | jaod 859 |
. . . . . . 7
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → (((𝐹‘𝐵) = 0 ∨ (𝐹‘𝐵) ∈ (1...𝑁)) → (𝐹‘𝐵) ∈ (1...𝑁))) |
56 | 24, 55 | biimtrid 242 |
. . . . . 6
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ((𝐹‘𝐵) ∈ 𝑊 → (𝐹‘𝐵) ∈ (1...𝑁))) |
57 | 7, 56 | mpd 15 |
. . . . 5
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → (𝐹‘𝐵) ∈ (1...𝑁)) |
58 | | f1ofn 6849 |
. . . . . . . . . 10
⊢ (𝐹:𝐶–1-1-onto→𝑊 → 𝐹 Fn 𝐶) |
59 | 58 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) → 𝐹 Fn 𝐶) |
60 | | 3simpc 1149 |
. . . . . . . . 9
⊢ ((𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) |
61 | 59, 60 | anim12i 613 |
. . . . . . . 8
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → (𝐹 Fn 𝐶 ∧ (𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶))) |
62 | | 3anass 1094 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐶 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ (𝐹 Fn 𝐶 ∧ (𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶))) |
63 | 61, 62 | sylibr 234 |
. . . . . . 7
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → (𝐹 Fn 𝐶 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) |
64 | | fnimapr 6991 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐶 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐹 “ {𝑋, 𝐵}) = {(𝐹‘𝑋), (𝐹‘𝐵)}) |
65 | 63, 64 | syl 17 |
. . . . . 6
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → (𝐹 “ {𝑋, 𝐵}) = {(𝐹‘𝑋), (𝐹‘𝐵)}) |
66 | | simpr 484 |
. . . . . . . 8
⊢ ((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) → (𝐹‘𝑋) = 0) |
67 | 66 | adantr 480 |
. . . . . . 7
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → (𝐹‘𝑋) = 0) |
68 | 67 | preq1d 4743 |
. . . . . 6
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → {(𝐹‘𝑋), (𝐹‘𝐵)} = {0, (𝐹‘𝐵)}) |
69 | 65, 68 | eqtrd 2774 |
. . . . 5
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → (𝐹 “ {𝑋, 𝐵}) = {0, (𝐹‘𝐵)}) |
70 | 2, 57, 69 | rspcedvdw 3624 |
. . . 4
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ∃𝑧 ∈ (1...𝑁)(𝐹 “ {𝑋, 𝐵}) = {0, 𝑧}) |
71 | 70 | ex 412 |
. . 3
⊢ ((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) → ((𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ∃𝑧 ∈ (1...𝑁)(𝐹 “ {𝑋, 𝐵}) = {0, 𝑧})) |
72 | | neeq1 3000 |
. . . . 5
⊢ (𝐴 = 𝑋 → (𝐴 ≠ 𝐵 ↔ 𝑋 ≠ 𝐵)) |
73 | | eleq1 2826 |
. . . . 5
⊢ (𝐴 = 𝑋 → (𝐴 ∈ 𝐶 ↔ 𝑋 ∈ 𝐶)) |
74 | 72, 73 | 3anbi12d 1436 |
. . . 4
⊢ (𝐴 = 𝑋 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶))) |
75 | | preq1 4737 |
. . . . . . 7
⊢ (𝐴 = 𝑋 → {𝐴, 𝐵} = {𝑋, 𝐵}) |
76 | 75 | imaeq2d 6079 |
. . . . . 6
⊢ (𝐴 = 𝑋 → (𝐹 “ {𝐴, 𝐵}) = (𝐹 “ {𝑋, 𝐵})) |
77 | 76 | eqeq1d 2736 |
. . . . 5
⊢ (𝐴 = 𝑋 → ((𝐹 “ {𝐴, 𝐵}) = {0, 𝑧} ↔ (𝐹 “ {𝑋, 𝐵}) = {0, 𝑧})) |
78 | 77 | rexbidv 3176 |
. . . 4
⊢ (𝐴 = 𝑋 → (∃𝑧 ∈ (1...𝑁)(𝐹 “ {𝐴, 𝐵}) = {0, 𝑧} ↔ ∃𝑧 ∈ (1...𝑁)(𝐹 “ {𝑋, 𝐵}) = {0, 𝑧})) |
79 | 74, 78 | imbi12d 344 |
. . 3
⊢ (𝐴 = 𝑋 → (((𝐴 ≠ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ∃𝑧 ∈ (1...𝑁)(𝐹 “ {𝐴, 𝐵}) = {0, 𝑧}) ↔ ((𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ∃𝑧 ∈ (1...𝑁)(𝐹 “ {𝑋, 𝐵}) = {0, 𝑧}))) |
80 | 71, 79 | imbitrrid 246 |
. 2
⊢ (𝐴 = 𝑋 → ((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) → ((𝐴 ≠ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ∃𝑧 ∈ (1...𝑁)(𝐹 “ {𝐴, 𝐵}) = {0, 𝑧}))) |
81 | 80 | 3imp 1110 |
1
⊢ ((𝐴 = 𝑋 ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ∃𝑧 ∈ (1...𝑁)(𝐹 “ {𝐴, 𝐵}) = {0, 𝑧}) |