Step |
Hyp |
Ref |
Expression |
1 |
|
isuspgr.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
isuspgr.e |
⊢ 𝐸 = ( iEdg ‘ 𝐺 ) |
3 |
|
df-usgr |
⊢ USGraph = { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 –1-1→ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } } |
4 |
3
|
eleq2i |
⊢ ( 𝐺 ∈ USGraph ↔ 𝐺 ∈ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 –1-1→ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } } ) |
5 |
|
fveq2 |
⊢ ( ℎ = 𝐺 → ( iEdg ‘ ℎ ) = ( iEdg ‘ 𝐺 ) ) |
6 |
5 2
|
eqtr4di |
⊢ ( ℎ = 𝐺 → ( iEdg ‘ ℎ ) = 𝐸 ) |
7 |
5
|
dmeqd |
⊢ ( ℎ = 𝐺 → dom ( iEdg ‘ ℎ ) = dom ( iEdg ‘ 𝐺 ) ) |
8 |
2
|
eqcomi |
⊢ ( iEdg ‘ 𝐺 ) = 𝐸 |
9 |
8
|
dmeqi |
⊢ dom ( iEdg ‘ 𝐺 ) = dom 𝐸 |
10 |
7 9
|
eqtrdi |
⊢ ( ℎ = 𝐺 → dom ( iEdg ‘ ℎ ) = dom 𝐸 ) |
11 |
|
fveq2 |
⊢ ( ℎ = 𝐺 → ( Vtx ‘ ℎ ) = ( Vtx ‘ 𝐺 ) ) |
12 |
11 1
|
eqtr4di |
⊢ ( ℎ = 𝐺 → ( Vtx ‘ ℎ ) = 𝑉 ) |
13 |
12
|
pweqd |
⊢ ( ℎ = 𝐺 → 𝒫 ( Vtx ‘ ℎ ) = 𝒫 𝑉 ) |
14 |
13
|
difeq1d |
⊢ ( ℎ = 𝐺 → ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) = ( 𝒫 𝑉 ∖ { ∅ } ) ) |
15 |
14
|
rabeqdv |
⊢ ( ℎ = 𝐺 → { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) |
16 |
6 10 15
|
f1eq123d |
⊢ ( ℎ = 𝐺 → ( ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) |
17 |
|
fvexd |
⊢ ( 𝑔 = ℎ → ( Vtx ‘ 𝑔 ) ∈ V ) |
18 |
|
fveq2 |
⊢ ( 𝑔 = ℎ → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ ℎ ) ) |
19 |
|
fvexd |
⊢ ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) → ( iEdg ‘ 𝑔 ) ∈ V ) |
20 |
|
fveq2 |
⊢ ( 𝑔 = ℎ → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ ℎ ) ) |
21 |
20
|
adantr |
⊢ ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ ℎ ) ) |
22 |
|
simpr |
⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → 𝑒 = ( iEdg ‘ ℎ ) ) |
23 |
22
|
dmeqd |
⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → dom 𝑒 = dom ( iEdg ‘ ℎ ) ) |
24 |
|
pweq |
⊢ ( 𝑣 = ( Vtx ‘ ℎ ) → 𝒫 𝑣 = 𝒫 ( Vtx ‘ ℎ ) ) |
25 |
24
|
ad2antlr |
⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → 𝒫 𝑣 = 𝒫 ( Vtx ‘ ℎ ) ) |
26 |
25
|
difeq1d |
⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → ( 𝒫 𝑣 ∖ { ∅ } ) = ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ) |
27 |
26
|
rabeqdv |
⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) |
28 |
22 23 27
|
f1eq123d |
⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → ( 𝑒 : dom 𝑒 –1-1→ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) |
29 |
19 21 28
|
sbcied2 |
⊢ ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) → ( [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 –1-1→ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) |
30 |
17 18 29
|
sbcied2 |
⊢ ( 𝑔 = ℎ → ( [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 –1-1→ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) |
31 |
30
|
cbvabv |
⊢ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 –1-1→ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } } = { ℎ ∣ ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } } |
32 |
16 31
|
elab2g |
⊢ ( 𝐺 ∈ 𝑈 → ( 𝐺 ∈ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 –1-1→ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } } ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) |
33 |
4 32
|
syl5bb |
⊢ ( 𝐺 ∈ 𝑈 → ( 𝐺 ∈ USGraph ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) |