Step | Hyp | Ref
| Expression |
1 | | simplr 788 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐴 ∈ 𝑋) |
2 | | prex 4836 |
. . . . . 6
⊢ {𝐵, 𝐶} ∈ V |
3 | | f1osng 6089 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ {𝐵, 𝐶} ∈ V) → {〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1-onto→{{𝐵, 𝐶}}) |
4 | 1, 2, 3 | sylancl 693 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → {〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1-onto→{{𝐵, 𝐶}}) |
5 | | f1of1 6049 |
. . . . 5
⊢
({〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1-onto→{{𝐵, 𝐶}} → {〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1→{{𝐵, 𝐶}}) |
6 | 4, 5 | syl 17 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → {〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1→{{𝐵, 𝐶}}) |
7 | | prssi 4293 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {𝐵, 𝐶} ⊆ 𝑉) |
8 | 7 | adantl 481 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → {𝐵, 𝐶} ⊆ 𝑉) |
9 | 2 | elpw 4114 |
. . . . . . . 8
⊢ ({𝐵, 𝐶} ∈ 𝒫 𝑉 ↔ {𝐵, 𝐶} ⊆ 𝑉) |
10 | 8, 9 | sylibr 223 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → {𝐵, 𝐶} ∈ 𝒫 𝑉) |
11 | | prnzg 4254 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑉 → {𝐵, 𝐶} ≠ ∅) |
12 | 11 | ad2antrl 760 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → {𝐵, 𝐶} ≠ ∅) |
13 | | eldifsn 4260 |
. . . . . . 7
⊢ ({𝐵, 𝐶} ∈ (𝒫 𝑉 ∖ {∅}) ↔ ({𝐵, 𝐶} ∈ 𝒫 𝑉 ∧ {𝐵, 𝐶} ≠ ∅)) |
14 | 10, 12, 13 | sylanbrc 695 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → {𝐵, 𝐶} ∈ (𝒫 𝑉 ∖ {∅})) |
15 | | hashprlei 13107 |
. . . . . . . 8
⊢ ({𝐵, 𝐶} ∈ Fin ∧ (#‘{𝐵, 𝐶}) ≤ 2) |
16 | 15 | simpri 477 |
. . . . . . 7
⊢
(#‘{𝐵, 𝐶}) ≤ 2 |
17 | 16 | a1i 11 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (#‘{𝐵, 𝐶}) ≤ 2) |
18 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = {𝐵, 𝐶} → (#‘𝑥) = (#‘{𝐵, 𝐶})) |
19 | 18 | breq1d 4593 |
. . . . . . 7
⊢ (𝑥 = {𝐵, 𝐶} → ((#‘𝑥) ≤ 2 ↔ (#‘{𝐵, 𝐶}) ≤ 2)) |
20 | 19 | elrab 3331 |
. . . . . 6
⊢ ({𝐵, 𝐶} ∈ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} ↔ ({𝐵, 𝐶} ∈ (𝒫 𝑉 ∖ {∅}) ∧ (#‘{𝐵, 𝐶}) ≤ 2)) |
21 | 14, 17, 20 | sylanbrc 695 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → {𝐵, 𝐶} ∈ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) |
22 | 21 | snssd 4281 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → {{𝐵, 𝐶}} ⊆ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) |
23 | | f1ss 6019 |
. . . 4
⊢
(({〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1→{{𝐵, 𝐶}} ∧ {{𝐵, 𝐶}} ⊆ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) → {〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) |
24 | 6, 22, 23 | syl2anc 691 |
. . 3
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → {〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) |
25 | | f1dm 6018 |
. . . 4
⊢
({〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} → dom
{〈𝐴, {𝐵, 𝐶}〉} = {𝐴}) |
26 | | f1eq2 6010 |
. . . 4
⊢ (dom
{〈𝐴, {𝐵, 𝐶}〉} = {𝐴} → ({〈𝐴, {𝐵, 𝐶}〉}:dom {〈𝐴, {𝐵, 𝐶}〉}–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} ↔ {〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2})) |
27 | 24, 25, 26 | 3syl 18 |
. . 3
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ({〈𝐴, {𝐵, 𝐶}〉}:dom {〈𝐴, {𝐵, 𝐶}〉}–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} ↔ {〈𝐴, {𝐵, 𝐶}〉}:{𝐴}–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2})) |
28 | 24, 27 | mpbird 246 |
. 2
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → {〈𝐴, {𝐵, 𝐶}〉}:dom {〈𝐴, {𝐵, 𝐶}〉}–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) |
29 | | simpll 786 |
. . 3
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝑉 ∈ 𝑊) |
30 | | snex 4835 |
. . 3
⊢
{〈𝐴, {𝐵, 𝐶}〉} ∈ V |
31 | | isuslgra 25872 |
. . 3
⊢ ((𝑉 ∈ 𝑊 ∧ {〈𝐴, {𝐵, 𝐶}〉} ∈ V) → (𝑉 USLGrph {〈𝐴, {𝐵, 𝐶}〉} ↔ {〈𝐴, {𝐵, 𝐶}〉}:dom {〈𝐴, {𝐵, 𝐶}〉}–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2})) |
32 | 29, 30, 31 | sylancl 693 |
. 2
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑉 USLGrph {〈𝐴, {𝐵, 𝐶}〉} ↔ {〈𝐴, {𝐵, 𝐶}〉}:dom {〈𝐴, {𝐵, 𝐶}〉}–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2})) |
33 | 28, 32 | mpbird 246 |
1
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝑉 USLGrph {〈𝐴, {𝐵, 𝐶}〉}) |