Step |
Hyp |
Ref |
Expression |
1 |
|
fusgrmaxsize.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
fusgrmaxsize.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
|
usgrsscusgra.h |
⊢ 𝑉 = ( Vtx ‘ 𝐻 ) |
4 |
|
usgrsscusgra.f |
⊢ 𝐹 = ( Edg ‘ 𝐻 ) |
5 |
1 2
|
usgredg |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑒 ∈ 𝐸 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) |
6 |
3 4
|
iscusgredg |
⊢ ( 𝐻 ∈ ComplUSGraph ↔ ( 𝐻 ∈ USGraph ∧ ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑘 } ) { 𝑛 , 𝑘 } ∈ 𝐹 ) ) |
7 |
|
sneq |
⊢ ( 𝑘 = 𝑎 → { 𝑘 } = { 𝑎 } ) |
8 |
7
|
difeq2d |
⊢ ( 𝑘 = 𝑎 → ( 𝑉 ∖ { 𝑘 } ) = ( 𝑉 ∖ { 𝑎 } ) ) |
9 |
|
preq2 |
⊢ ( 𝑘 = 𝑎 → { 𝑛 , 𝑘 } = { 𝑛 , 𝑎 } ) |
10 |
9
|
eleq1d |
⊢ ( 𝑘 = 𝑎 → ( { 𝑛 , 𝑘 } ∈ 𝐹 ↔ { 𝑛 , 𝑎 } ∈ 𝐹 ) ) |
11 |
8 10
|
raleqbidv |
⊢ ( 𝑘 = 𝑎 → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑘 } ) { 𝑛 , 𝑘 } ∈ 𝐹 ↔ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑎 } ) { 𝑛 , 𝑎 } ∈ 𝐹 ) ) |
12 |
11
|
rspcv |
⊢ ( 𝑎 ∈ 𝑉 → ( ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑘 } ) { 𝑛 , 𝑘 } ∈ 𝐹 → ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑎 } ) { 𝑛 , 𝑎 } ∈ 𝐹 ) ) |
13 |
|
simpl |
⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) → 𝑎 ≠ 𝑏 ) |
14 |
13
|
necomd |
⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) → 𝑏 ≠ 𝑎 ) |
15 |
14
|
anim2i |
⊢ ( ( 𝑏 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( 𝑏 ∈ 𝑉 ∧ 𝑏 ≠ 𝑎 ) ) |
16 |
|
eldifsn |
⊢ ( 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ↔ ( 𝑏 ∈ 𝑉 ∧ 𝑏 ≠ 𝑎 ) ) |
17 |
15 16
|
sylibr |
⊢ ( ( 𝑏 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) |
18 |
|
preq1 |
⊢ ( 𝑛 = 𝑏 → { 𝑛 , 𝑎 } = { 𝑏 , 𝑎 } ) |
19 |
18
|
eleq1d |
⊢ ( 𝑛 = 𝑏 → ( { 𝑛 , 𝑎 } ∈ 𝐹 ↔ { 𝑏 , 𝑎 } ∈ 𝐹 ) ) |
20 |
19
|
rspcv |
⊢ ( 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑎 } ) { 𝑛 , 𝑎 } ∈ 𝐹 → { 𝑏 , 𝑎 } ∈ 𝐹 ) ) |
21 |
17 20
|
syl |
⊢ ( ( 𝑏 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑎 } ) { 𝑛 , 𝑎 } ∈ 𝐹 → { 𝑏 , 𝑎 } ∈ 𝐹 ) ) |
22 |
|
prcom |
⊢ { 𝑎 , 𝑏 } = { 𝑏 , 𝑎 } |
23 |
22
|
eqeq2i |
⊢ ( 𝑒 = { 𝑎 , 𝑏 } ↔ 𝑒 = { 𝑏 , 𝑎 } ) |
24 |
|
eqcom |
⊢ ( 𝑒 = { 𝑏 , 𝑎 } ↔ { 𝑏 , 𝑎 } = 𝑒 ) |
25 |
23 24
|
sylbb |
⊢ ( 𝑒 = { 𝑎 , 𝑏 } → { 𝑏 , 𝑎 } = 𝑒 ) |
26 |
25
|
eleq1d |
⊢ ( 𝑒 = { 𝑎 , 𝑏 } → ( { 𝑏 , 𝑎 } ∈ 𝐹 ↔ 𝑒 ∈ 𝐹 ) ) |
27 |
26
|
biimpd |
⊢ ( 𝑒 = { 𝑎 , 𝑏 } → ( { 𝑏 , 𝑎 } ∈ 𝐹 → 𝑒 ∈ 𝐹 ) ) |
28 |
27
|
ad2antll |
⊢ ( ( 𝑏 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( { 𝑏 , 𝑎 } ∈ 𝐹 → 𝑒 ∈ 𝐹 ) ) |
29 |
21 28
|
syld |
⊢ ( ( 𝑏 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑎 } ) { 𝑛 , 𝑎 } ∈ 𝐹 → 𝑒 ∈ 𝐹 ) ) |
30 |
12 29
|
syl9 |
⊢ ( 𝑎 ∈ 𝑉 → ( ( 𝑏 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑘 } ) { 𝑛 , 𝑘 } ∈ 𝐹 → 𝑒 ∈ 𝐹 ) ) ) |
31 |
30
|
impl |
⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑘 } ) { 𝑛 , 𝑘 } ∈ 𝐹 → 𝑒 ∈ 𝐹 ) ) |
32 |
31
|
adantld |
⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( ( 𝐻 ∈ USGraph ∧ ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑘 } ) { 𝑛 , 𝑘 } ∈ 𝐹 ) → 𝑒 ∈ 𝐹 ) ) |
33 |
6 32
|
syl5bi |
⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( 𝐻 ∈ ComplUSGraph → 𝑒 ∈ 𝐹 ) ) |
34 |
33
|
ex |
⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) → ( 𝐻 ∈ ComplUSGraph → 𝑒 ∈ 𝐹 ) ) ) |
35 |
34
|
rexlimivv |
⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) → ( 𝐻 ∈ ComplUSGraph → 𝑒 ∈ 𝐹 ) ) |
36 |
5 35
|
syl |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑒 ∈ 𝐸 ) → ( 𝐻 ∈ ComplUSGraph → 𝑒 ∈ 𝐹 ) ) |
37 |
36
|
impancom |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → ( 𝑒 ∈ 𝐸 → 𝑒 ∈ 𝐹 ) ) |
38 |
37
|
ssrdv |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → 𝐸 ⊆ 𝐹 ) |