Step | Hyp | Ref
| Expression |
1 | | simpllr 795 |
. . . . . . 7
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐵 ≠ 𝐶) → 𝐴 ∈ 𝑋) |
2 | | prex 4836 |
. . . . . . 7
⊢ {𝐵, 𝐶} ∈ V |
3 | | f1osng 6089 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ {𝐵, 𝐶} ∈ V) → {〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1-onto→{{𝐵, 𝐶}}) |
4 | 1, 2, 3 | sylancl 693 |
. . . . . 6
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐵 ≠ 𝐶) → {〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1-onto→{{𝐵, 𝐶}}) |
5 | | f1of1 6049 |
. . . . . 6
⊢
({〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1-onto→{{𝐵, 𝐶}} → {〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1→{{𝐵, 𝐶}}) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐵 ≠ 𝐶) → {〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1→{{𝐵, 𝐶}}) |
7 | | prelpwi 4842 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {𝐵, 𝐶} ∈ 𝒫 𝑉) |
8 | 7 | adantl 481 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → {𝐵, 𝐶} ∈ 𝒫 𝑉) |
9 | 8 | adantr 480 |
. . . . . . 7
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐵 ≠ 𝐶) → {𝐵, 𝐶} ∈ 𝒫 𝑉) |
10 | | hashprgOLD 13044 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐵 ≠ 𝐶 ↔ (#‘{𝐵, 𝐶}) = 2)) |
11 | 10 | adantl 481 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐵 ≠ 𝐶 ↔ (#‘{𝐵, 𝐶}) = 2)) |
12 | 11 | biimpa 500 |
. . . . . . 7
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐵 ≠ 𝐶) → (#‘{𝐵, 𝐶}) = 2) |
13 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = {𝐵, 𝐶} → (#‘𝑥) = (#‘{𝐵, 𝐶})) |
14 | 13 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑥 = {𝐵, 𝐶} → ((#‘𝑥) = 2 ↔ (#‘{𝐵, 𝐶}) = 2)) |
15 | 14 | elrab 3331 |
. . . . . . 7
⊢ ({𝐵, 𝐶} ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ↔ ({𝐵, 𝐶} ∈ 𝒫 𝑉 ∧ (#‘{𝐵, 𝐶}) = 2)) |
16 | 9, 12, 15 | sylanbrc 695 |
. . . . . 6
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐵 ≠ 𝐶) → {𝐵, 𝐶} ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
17 | 16 | snssd 4281 |
. . . . 5
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐵 ≠ 𝐶) → {{𝐵, 𝐶}} ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
18 | | f1ss 6019 |
. . . . 5
⊢
(({〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1→{{𝐵, 𝐶}} ∧ {{𝐵, 𝐶}} ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) → {〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
19 | 6, 17, 18 | syl2anc 691 |
. . . 4
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐵 ≠ 𝐶) → {〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
20 | | f1dm 6018 |
. . . . 5
⊢
({〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → dom {〈𝐴, {𝐵, 𝐶}〉} = {𝐴}) |
21 | | f1eq2 6010 |
. . . . 5
⊢ (dom
{〈𝐴, {𝐵, 𝐶}〉} = {𝐴} → ({〈𝐴, {𝐵, 𝐶}〉}:dom {〈𝐴, {𝐵, 𝐶}〉}–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ↔ {〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
22 | 19, 20, 21 | 3syl 18 |
. . . 4
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐵 ≠ 𝐶) → ({〈𝐴, {𝐵, 𝐶}〉}:dom {〈𝐴, {𝐵, 𝐶}〉}–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ↔ {〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
23 | 19, 22 | mpbird 246 |
. . 3
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐵 ≠ 𝐶) → {〈𝐴, {𝐵, 𝐶}〉}:dom {〈𝐴, {𝐵, 𝐶}〉}–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
24 | | simpll 786 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝑉 ∈ 𝑊) |
25 | | snex 4835 |
. . . . 5
⊢
{〈𝐴, {𝐵, 𝐶}〉} ∈ V |
26 | | isusgra0 25876 |
. . . . 5
⊢ ((𝑉 ∈ 𝑊 ∧ {〈𝐴, {𝐵, 𝐶}〉} ∈ V) → (𝑉 USGrph {〈𝐴, {𝐵, 𝐶}〉} ↔ {〈𝐴, {𝐵, 𝐶}〉}:dom {〈𝐴, {𝐵, 𝐶}〉}–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
27 | 24, 25, 26 | sylancl 693 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑉 USGrph {〈𝐴, {𝐵, 𝐶}〉} ↔ {〈𝐴, {𝐵, 𝐶}〉}:dom {〈𝐴, {𝐵, 𝐶}〉}–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
28 | 27 | adantr 480 |
. . 3
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐵 ≠ 𝐶) → (𝑉 USGrph {〈𝐴, {𝐵, 𝐶}〉} ↔ {〈𝐴, {𝐵, 𝐶}〉}:dom {〈𝐴, {𝐵, 𝐶}〉}–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
29 | 23, 28 | mpbird 246 |
. 2
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐵 ≠ 𝐶) → 𝑉 USGrph {〈𝐴, {𝐵, 𝐶}〉}) |
30 | 29 | ex 449 |
1
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐵 ≠ 𝐶 → 𝑉 USGrph {〈𝐴, {𝐵, 𝐶}〉})) |