Step |
Hyp |
Ref |
Expression |
1 |
|
upgredg.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
upgredg.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
1 2
|
upgredg |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝑎 , 𝑏 } ) |
4 |
3
|
3adant3 |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝑎 , 𝑏 } ) |
5 |
|
ssprsseq |
⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } ⊆ { 𝑎 , 𝑏 } ↔ { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) ) |
6 |
5
|
biimpd |
⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } ⊆ { 𝑎 , 𝑏 } → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) ) |
7 |
|
sseq2 |
⊢ ( 𝐶 = { 𝑎 , 𝑏 } → ( { 𝐴 , 𝐵 } ⊆ 𝐶 ↔ { 𝐴 , 𝐵 } ⊆ { 𝑎 , 𝑏 } ) ) |
8 |
|
eqeq2 |
⊢ ( 𝐶 = { 𝑎 , 𝑏 } → ( { 𝐴 , 𝐵 } = 𝐶 ↔ { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) ) |
9 |
7 8
|
imbi12d |
⊢ ( 𝐶 = { 𝑎 , 𝑏 } → ( ( { 𝐴 , 𝐵 } ⊆ 𝐶 → { 𝐴 , 𝐵 } = 𝐶 ) ↔ ( { 𝐴 , 𝐵 } ⊆ { 𝑎 , 𝑏 } → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) ) ) |
10 |
6 9
|
syl5ibr |
⊢ ( 𝐶 = { 𝑎 , 𝑏 } → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } ⊆ 𝐶 → { 𝐴 , 𝐵 } = 𝐶 ) ) ) |
11 |
10
|
com23 |
⊢ ( 𝐶 = { 𝑎 , 𝑏 } → ( { 𝐴 , 𝐵 } ⊆ 𝐶 → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 ) ) ) |
12 |
11
|
a1i |
⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝐶 = { 𝑎 , 𝑏 } → ( { 𝐴 , 𝐵 } ⊆ 𝐶 → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 ) ) ) ) |
13 |
12
|
rexlimivv |
⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝑎 , 𝑏 } → ( { 𝐴 , 𝐵 } ⊆ 𝐶 → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 ) ) ) |
14 |
13
|
com12 |
⊢ ( { 𝐴 , 𝐵 } ⊆ 𝐶 → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝑎 , 𝑏 } → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 ) ) ) |
15 |
14
|
3ad2ant3 |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝑎 , 𝑏 } → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 ) ) ) |
16 |
4 15
|
mpd |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 ) ) |
17 |
16
|
imp |
⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ) → { 𝐴 , 𝐵 } = 𝐶 ) |