Step |
Hyp |
Ref |
Expression |
1 |
|
griedg0prc.u |
⊢ 𝑈 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } |
2 |
1
|
eleq2i |
⊢ ( 𝑔 ∈ 𝑈 ↔ 𝑔 ∈ { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } ) |
3 |
|
elopab |
⊢ ( 𝑔 ∈ { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } ↔ ∃ 𝑣 ∃ 𝑒 ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ ∧ 𝑒 : ∅ ⟶ ∅ ) ) |
4 |
2 3
|
bitri |
⊢ ( 𝑔 ∈ 𝑈 ↔ ∃ 𝑣 ∃ 𝑒 ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ ∧ 𝑒 : ∅ ⟶ ∅ ) ) |
5 |
|
opex |
⊢ ⟨ 𝑣 , 𝑒 ⟩ ∈ V |
6 |
5
|
a1i |
⊢ ( 𝑒 : ∅ ⟶ ∅ → ⟨ 𝑣 , 𝑒 ⟩ ∈ V ) |
7 |
|
vex |
⊢ 𝑣 ∈ V |
8 |
|
vex |
⊢ 𝑒 ∈ V |
9 |
7 8
|
opiedgfvi |
⊢ ( iEdg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = 𝑒 |
10 |
|
f0bi |
⊢ ( 𝑒 : ∅ ⟶ ∅ ↔ 𝑒 = ∅ ) |
11 |
10
|
biimpi |
⊢ ( 𝑒 : ∅ ⟶ ∅ → 𝑒 = ∅ ) |
12 |
9 11
|
eqtrid |
⊢ ( 𝑒 : ∅ ⟶ ∅ → ( iEdg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = ∅ ) |
13 |
6 12
|
usgr0e |
⊢ ( 𝑒 : ∅ ⟶ ∅ → ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ) |
14 |
13
|
adantl |
⊢ ( ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ ∧ 𝑒 : ∅ ⟶ ∅ ) → ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ) |
15 |
|
eleq1 |
⊢ ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ → ( 𝑔 ∈ USGraph ↔ ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ) ) |
16 |
15
|
adantr |
⊢ ( ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ ∧ 𝑒 : ∅ ⟶ ∅ ) → ( 𝑔 ∈ USGraph ↔ ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ) ) |
17 |
14 16
|
mpbird |
⊢ ( ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ ∧ 𝑒 : ∅ ⟶ ∅ ) → 𝑔 ∈ USGraph ) |
18 |
17
|
exlimivv |
⊢ ( ∃ 𝑣 ∃ 𝑒 ( 𝑔 = ⟨ 𝑣 , 𝑒 ⟩ ∧ 𝑒 : ∅ ⟶ ∅ ) → 𝑔 ∈ USGraph ) |
19 |
4 18
|
sylbi |
⊢ ( 𝑔 ∈ 𝑈 → 𝑔 ∈ USGraph ) |
20 |
19
|
ssriv |
⊢ 𝑈 ⊆ USGraph |