Step |
Hyp |
Ref |
Expression |
1 |
|
uspgr1e.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
uspgr1e.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑋 ) |
3 |
|
uspgr1e.b |
⊢ ( 𝜑 → 𝐵 ∈ 𝑉 ) |
4 |
|
uspgr1e.c |
⊢ ( 𝜑 → 𝐶 ∈ 𝑉 ) |
5 |
|
uspgr1e.e |
⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } ) |
6 |
|
prex |
⊢ { 𝐵 , 𝐶 } ∈ V |
7 |
6
|
snid |
⊢ { 𝐵 , 𝐶 } ∈ { { 𝐵 , 𝐶 } } |
8 |
|
f1sng |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ { 𝐵 , 𝐶 } ∈ { { 𝐵 , 𝐶 } } ) → { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } : { 𝐴 } –1-1→ { { 𝐵 , 𝐶 } } ) |
9 |
2 7 8
|
sylancl |
⊢ ( 𝜑 → { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } : { 𝐴 } –1-1→ { { 𝐵 , 𝐶 } } ) |
10 |
3 4
|
prssd |
⊢ ( 𝜑 → { 𝐵 , 𝐶 } ⊆ 𝑉 ) |
11 |
10 1
|
sseqtrdi |
⊢ ( 𝜑 → { 𝐵 , 𝐶 } ⊆ ( Vtx ‘ 𝐺 ) ) |
12 |
6
|
elpw |
⊢ ( { 𝐵 , 𝐶 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) ↔ { 𝐵 , 𝐶 } ⊆ ( Vtx ‘ 𝐺 ) ) |
13 |
11 12
|
sylibr |
⊢ ( 𝜑 → { 𝐵 , 𝐶 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) ) |
14 |
13 3
|
upgr1elem |
⊢ ( 𝜑 → { { 𝐵 , 𝐶 } } ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
15 |
|
f1ss |
⊢ ( ( { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } : { 𝐴 } –1-1→ { { 𝐵 , 𝐶 } } ∧ { { 𝐵 , 𝐶 } } ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) → { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } : { 𝐴 } –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
16 |
9 14 15
|
syl2anc |
⊢ ( 𝜑 → { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } : { 𝐴 } –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
17 |
6
|
a1i |
⊢ ( 𝜑 → { 𝐵 , 𝐶 } ∈ V ) |
18 |
17 3
|
upgr1elem |
⊢ ( 𝜑 → { { 𝐵 , 𝐶 } } ⊆ { 𝑥 ∈ ( V ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
19 |
|
f1ss |
⊢ ( ( { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } : { 𝐴 } –1-1→ { { 𝐵 , 𝐶 } } ∧ { { 𝐵 , 𝐶 } } ⊆ { 𝑥 ∈ ( V ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) → { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } : { 𝐴 } –1-1→ { 𝑥 ∈ ( V ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
20 |
9 18 19
|
syl2anc |
⊢ ( 𝜑 → { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } : { 𝐴 } –1-1→ { 𝑥 ∈ ( V ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
21 |
|
f1dm |
⊢ ( { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } : { 𝐴 } –1-1→ { 𝑥 ∈ ( V ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → dom { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } = { 𝐴 } ) |
22 |
|
f1eq2 |
⊢ ( dom { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } = { 𝐴 } → ( { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } : dom { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ↔ { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } : { 𝐴 } –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) ) |
23 |
20 21 22
|
3syl |
⊢ ( 𝜑 → ( { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } : dom { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ↔ { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } : { 𝐴 } –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) ) |
24 |
16 23
|
mpbird |
⊢ ( 𝜑 → { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } : dom { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
25 |
5
|
dmeqd |
⊢ ( 𝜑 → dom ( iEdg ‘ 𝐺 ) = dom { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } ) |
26 |
|
eqidd |
⊢ ( 𝜑 → { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } = { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
27 |
5 25 26
|
f1eq123d |
⊢ ( 𝜑 → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ↔ { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } : dom { 〈 𝐴 , { 𝐵 , 𝐶 } 〉 } –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) ) |
28 |
24 27
|
mpbird |
⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
29 |
1
|
1vgrex |
⊢ ( 𝐵 ∈ 𝑉 → 𝐺 ∈ V ) |
30 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
31 |
|
eqid |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) |
32 |
30 31
|
isuspgr |
⊢ ( 𝐺 ∈ V → ( 𝐺 ∈ USPGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) ) |
33 |
3 29 32
|
3syl |
⊢ ( 𝜑 → ( 𝐺 ∈ USPGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) ) |
34 |
28 33
|
mpbird |
⊢ ( 𝜑 → 𝐺 ∈ USPGraph ) |