| Step | Hyp | Ref
| Expression |
| 1 | | preq2 4734 |
. . . . . 6
⊢ (𝑧 = (𝐹‘𝐵) → {0, 𝑧} = {0, (𝐹‘𝐵)}) |
| 2 | 1 | eqeq2d 2748 |
. . . . 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 1197 |
. . . . . . 7
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → 𝐵 ∈ 𝐶) |
| 7 | 5, 6 | ffvelcdmd 7105 |
. . . . . 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 47921 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (Vtx‘(StarGr‘𝑁)) = (0...𝑁)) |
| 13 | 11, 12 | ax-mp 5 |
. . . . . . . . . 10
⊢
(Vtx‘(StarGr‘𝑁)) = (0...𝑁) |
| 14 | 8, 10, 13 | 3eqtri 2769 |
. . . . . . . . 9
⊢ 𝑊 = (0...𝑁) |
| 15 | 14 | eleq2i 2833 |
. . . . . . . 8
⊢ ((𝐹‘𝐵) ∈ 𝑊 ↔ (𝐹‘𝐵) ∈ (0...𝑁)) |
| 16 | | fz0sn0fz1 13685 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (0...𝑁) = ({0} ∪
(1...𝑁))) |
| 17 | 11, 16 | ax-mp 5 |
. . . . . . . . 9
⊢
(0...𝑁) = ({0} ∪
(1...𝑁)) |
| 18 | 17 | eleq2i 2833 |
. . . . . . . 8
⊢ ((𝐹‘𝐵) ∈ (0...𝑁) ↔ (𝐹‘𝐵) ∈ ({0} ∪ (1...𝑁))) |
| 19 | | elun 4153 |
. . . . . . . . 9
⊢ ((𝐹‘𝐵) ∈ ({0} ∪ (1...𝑁)) ↔ ((𝐹‘𝐵) ∈ {0} ∨ (𝐹‘𝐵) ∈ (1...𝑁))) |
| 20 | | fvex 6919 |
. . . . . . . . . . 11
⊢ (𝐹‘𝐵) ∈ V |
| 21 | 20 | elsn 4641 |
. . . . . . . . . 10
⊢ ((𝐹‘𝐵) ∈ {0} ↔ (𝐹‘𝐵) = 0) |
| 22 | 21 | orbi1i 914 |
. . . . . . . . 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 2749 |
. . . . . . . . . . 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 7290 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝐶–1-1→𝑊 ↔ (𝐹:𝐶⟶𝑊 ∧ ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐶 (𝑎 ≠ 𝑏 → (𝐹‘𝑎) ≠ (𝐹‘𝑏)))) |
| 30 | | simpl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝐵) → 𝑎 = 𝑋) |
| 31 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
| 32 | 30, 31 | neeq12d 3002 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝐵) → (𝑎 ≠ 𝑏 ↔ 𝑋 ≠ 𝐵)) |
| 33 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝑋 → (𝐹‘𝑎) = (𝐹‘𝑋)) |
| 34 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝐵) → (𝐹‘𝑎) = (𝐹‘𝑋)) |
| 35 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = 𝐵 → (𝐹‘𝑏) = (𝐹‘𝐵)) |
| 36 | 35 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝐵) → (𝐹‘𝑏) = (𝐹‘𝐵)) |
| 37 | 34, 36 | neeq12d 3002 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝐵) → ((𝐹‘𝑎) ≠ (𝐹‘𝑏) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝐵))) |
| 38 | 32, 37 | imbi12d 344 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝐵) → ((𝑎 ≠ 𝑏 → (𝐹‘𝑎) ≠ (𝐹‘𝑏)) ↔ (𝑋 ≠ 𝐵 → (𝐹‘𝑋) ≠ (𝐹‘𝐵)))) |
| 39 | 38 | rspc2gv 3632 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐶 (𝑎 ≠ 𝑏 → (𝐹‘𝑎) ≠ (𝐹‘𝑏)) → (𝑋 ≠ 𝐵 → (𝐹‘𝑋) ≠ (𝐹‘𝐵)))) |
| 40 | 39 | 3adant1 1131 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐶 (𝑎 ≠ 𝑏 → (𝐹‘𝑎) ≠ (𝐹‘𝑏)) → (𝑋 ≠ 𝐵 → (𝐹‘𝑋) ≠ (𝐹‘𝐵)))) |
| 41 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ≠ 𝐵 → (𝐹‘𝑋) ≠ (𝐹‘𝐵)) → (𝑋 ≠ 𝐵 → (𝐹‘𝑋) ≠ (𝐹‘𝐵))) |
| 42 | | eqneqall 2951 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑋) = (𝐹‘𝐵) → ((𝐹‘𝑋) ≠ (𝐹‘𝐵) → (𝐹‘𝐵) ∈ (1...𝑁))) |
| 43 | 42 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝐵) = (𝐹‘𝑋) → ((𝐹‘𝑋) ≠ (𝐹‘𝐵) → (𝐹‘𝐵) ∈ (1...𝑁))) |
| 44 | 43 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑋) ≠ (𝐹‘𝐵) → ((𝐹‘𝐵) = (𝐹‘𝑋) → (𝐹‘𝐵) ∈ (1...𝑁))) |
| 45 | 41, 44 | syl6com 37 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ≠ 𝐵 → ((𝑋 ≠ 𝐵 → (𝐹‘𝑋) ≠ (𝐹‘𝐵)) → ((𝐹‘𝐵) = (𝐹‘𝑋) → (𝐹‘𝐵) ∈ (1...𝑁)))) |
| 46 | 45 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 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 860 |
. . . . . . 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 1151 |
. . . . . . . . 9
⊢ ((𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) |
| 61 | 59, 60 | anim12i 613 |
. . . . . . . 8
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → (𝐹 Fn 𝐶 ∧ (𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶))) |
| 62 | | 3anass 1095 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐶 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ (𝐹 Fn 𝐶 ∧ (𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶))) |
| 63 | 61, 62 | sylibr 234 |
. . . . . . 7
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → (𝐹 Fn 𝐶 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) |
| 64 | | fnimapr 6992 |
. . . . . . 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 4739 |
. . . . . 6
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → {(𝐹‘𝑋), (𝐹‘𝐵)} = {0, (𝐹‘𝐵)}) |
| 69 | 65, 68 | eqtrd 2777 |
. . . . 5
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → (𝐹 “ {𝑋, 𝐵}) = {0, (𝐹‘𝐵)}) |
| 70 | 2, 57, 69 | rspcedvdw 3625 |
. . . 4
⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ∃𝑧 ∈ (1...𝑁)(𝐹 “ {𝑋, 𝐵}) = {0, 𝑧}) |
| 71 | 70 | ex 412 |
. . 3
⊢ ((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) → ((𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ∃𝑧 ∈ (1...𝑁)(𝐹 “ {𝑋, 𝐵}) = {0, 𝑧})) |
| 72 | | neeq1 3003 |
. . . . 5
⊢ (𝐴 = 𝑋 → (𝐴 ≠ 𝐵 ↔ 𝑋 ≠ 𝐵)) |
| 73 | | eleq1 2829 |
. . . . 5
⊢ (𝐴 = 𝑋 → (𝐴 ∈ 𝐶 ↔ 𝑋 ∈ 𝐶)) |
| 74 | 72, 73 | 3anbi12d 1439 |
. . . 4
⊢ (𝐴 = 𝑋 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ (𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶))) |
| 75 | | preq1 4733 |
. . . . . . 7
⊢ (𝐴 = 𝑋 → {𝐴, 𝐵} = {𝑋, 𝐵}) |
| 76 | 75 | imaeq2d 6078 |
. . . . . 6
⊢ (𝐴 = 𝑋 → (𝐹 “ {𝐴, 𝐵}) = (𝐹 “ {𝑋, 𝐵})) |
| 77 | 76 | eqeq1d 2739 |
. . . . 5
⊢ (𝐴 = 𝑋 → ((𝐹 “ {𝐴, 𝐵}) = {0, 𝑧} ↔ (𝐹 “ {𝑋, 𝐵}) = {0, 𝑧})) |
| 78 | 77 | rexbidv 3179 |
. . . 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 1111 |
1
⊢ ((𝐴 = 𝑋 ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ∃𝑧 ∈ (1...𝑁)(𝐹 “ {𝐴, 𝐵}) = {0, 𝑧}) |