Proof of Theorem isubgr3stgrlem1
| Step | Hyp | Ref
| Expression |
| 1 | | isubgr3stgr.u |
. . . . . 6
⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) |
| 2 | | f1oeq2 6837 |
. . . . . 6
⊢ (𝑈 = (𝐺 NeighbVtx 𝑋) → (𝐻:𝑈–1-1-onto→𝑅 ↔ 𝐻:(𝐺 NeighbVtx 𝑋)–1-1-onto→𝑅)) |
| 3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢ (𝐻:𝑈–1-1-onto→𝑅 ↔ 𝐻:(𝐺 NeighbVtx 𝑋)–1-1-onto→𝑅) |
| 4 | 3 | biimpi 216 |
. . . 4
⊢ (𝐻:𝑈–1-1-onto→𝑅 → 𝐻:(𝐺 NeighbVtx 𝑋)–1-1-onto→𝑅) |
| 5 | 4 | 3ad2ant1 1134 |
. . 3
⊢ ((𝐻:𝑈–1-1-onto→𝑅 ∧ 𝑋 ∈ 𝑉 ∧ (𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅)) → 𝐻:(𝐺 NeighbVtx 𝑋)–1-1-onto→𝑅) |
| 6 | | simpl 482 |
. . . . 5
⊢ ((𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅) → 𝑌 ∈ 𝑊) |
| 7 | 6 | anim2i 617 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ (𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅)) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) |
| 8 | 7 | 3adant1 1131 |
. . 3
⊢ ((𝐻:𝑈–1-1-onto→𝑅 ∧ 𝑋 ∈ 𝑉 ∧ (𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅)) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) |
| 9 | | nbgrnself2 29377 |
. . . 4
⊢ 𝑋 ∉ (𝐺 NeighbVtx 𝑋) |
| 10 | 9 | a1i 11 |
. . 3
⊢ ((𝐻:𝑈–1-1-onto→𝑅 ∧ 𝑋 ∈ 𝑉 ∧ (𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅)) → 𝑋 ∉ (𝐺 NeighbVtx 𝑋)) |
| 11 | | simp3r 1203 |
. . 3
⊢ ((𝐻:𝑈–1-1-onto→𝑅 ∧ 𝑋 ∈ 𝑉 ∧ (𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅)) → 𝑌 ∉ 𝑅) |
| 12 | | isubgr3stgr.f |
. . . 4
⊢ 𝐹 = (𝐻 ∪ {〈𝑋, 𝑌〉}) |
| 13 | 12 | f1ounsn 7292 |
. . 3
⊢ ((𝐻:(𝐺 NeighbVtx 𝑋)–1-1-onto→𝑅 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ (𝐺 NeighbVtx 𝑋) ∧ 𝑌 ∉ 𝑅)) → 𝐹:((𝐺 NeighbVtx 𝑋) ∪ {𝑋})–1-1-onto→(𝑅 ∪ {𝑌})) |
| 14 | 5, 8, 10, 11, 13 | syl112anc 1376 |
. 2
⊢ ((𝐻:𝑈–1-1-onto→𝑅 ∧ 𝑋 ∈ 𝑉 ∧ (𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅)) → 𝐹:((𝐺 NeighbVtx 𝑋) ∪ {𝑋})–1-1-onto→(𝑅 ∪ {𝑌})) |
| 15 | | isubgr3stgr.c |
. . . 4
⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) |
| 16 | | isubgr3stgr.v |
. . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) |
| 17 | 16 | dfclnbgr4 47811 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑋) = ({𝑋} ∪ (𝐺 NeighbVtx 𝑋))) |
| 18 | 17 | 3ad2ant2 1135 |
. . . . 5
⊢ ((𝐻:𝑈–1-1-onto→𝑅 ∧ 𝑋 ∈ 𝑉 ∧ (𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅)) → (𝐺 ClNeighbVtx 𝑋) = ({𝑋} ∪ (𝐺 NeighbVtx 𝑋))) |
| 19 | | uncom 4158 |
. . . . 5
⊢ ({𝑋} ∪ (𝐺 NeighbVtx 𝑋)) = ((𝐺 NeighbVtx 𝑋) ∪ {𝑋}) |
| 20 | 18, 19 | eqtrdi 2793 |
. . . 4
⊢ ((𝐻:𝑈–1-1-onto→𝑅 ∧ 𝑋 ∈ 𝑉 ∧ (𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅)) → (𝐺 ClNeighbVtx 𝑋) = ((𝐺 NeighbVtx 𝑋) ∪ {𝑋})) |
| 21 | 15, 20 | eqtrid 2789 |
. . 3
⊢ ((𝐻:𝑈–1-1-onto→𝑅 ∧ 𝑋 ∈ 𝑉 ∧ (𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅)) → 𝐶 = ((𝐺 NeighbVtx 𝑋) ∪ {𝑋})) |
| 22 | 21 | f1oeq2d 6844 |
. 2
⊢ ((𝐻:𝑈–1-1-onto→𝑅 ∧ 𝑋 ∈ 𝑉 ∧ (𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅)) → (𝐹:𝐶–1-1-onto→(𝑅 ∪ {𝑌}) ↔ 𝐹:((𝐺 NeighbVtx 𝑋) ∪ {𝑋})–1-1-onto→(𝑅 ∪ {𝑌}))) |
| 23 | 14, 22 | mpbird 257 |
1
⊢ ((𝐻:𝑈–1-1-onto→𝑅 ∧ 𝑋 ∈ 𝑉 ∧ (𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅)) → 𝐹:𝐶–1-1-onto→(𝑅 ∪ {𝑌})) |