Metamath Proof Explorer

Theorem usgredgprvALT

Description: Alternate proof of usgredgprv , using usgredg2 instead of umgredgprv . (Contributed by Alexander van der Vekens, 19-Aug-2017) (Revised by AV, 16-Oct-2020) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses usgredg2.e ⊢ E = iEdg ⁡ G
usgredgprv.v ⊢ V = Vtx ⁡ G
Assertion usgredgprvALT ⊢ G ∈ USGraph ∧ X ∈ dom ⁡ E → E ⁡ X = M N → M ∈ V ∧ N ∈ V

Proof

Step Hyp Ref Expression
1 usgredg2.e ⊢ E = iEdg ⁡ G
2 usgredgprv.v ⊢ V = Vtx ⁡ G
3 1 2 usgrss ⊢ G ∈ USGraph ∧ X ∈ dom ⁡ E → E ⁡ X ⊆ V
4 1 usgredg2 ⊢ G ∈ USGraph ∧ X ∈ dom ⁡ E → E ⁡ X = 2
5 sseq1 ⊢ E ⁡ X = M N → E ⁡ X ⊆ V ↔ M N ⊆ V
6 fveq2 ⊢ E ⁡ X = M N → E ⁡ X = M N
7 6 eqeq1d ⊢ E ⁡ X = M N → E ⁡ X = 2 ↔ M N = 2
8 5 7 anbi12d ⊢ E ⁡ X = M N → E ⁡ X ⊆ V ∧ E ⁡ X = 2 ↔ M N ⊆ V ∧ M N = 2
9 eqid ⊢ M N = M N
10 9 hashprdifel ⊢ M N = 2 → M ∈ M N ∧ N ∈ M N ∧ M ≠ N
11 prssg ⊢ M ∈ M N ∧ N ∈ M N → M ∈ V ∧ N ∈ V ↔ M N ⊆ V
12 11 3adant3 ⊢ M ∈ M N ∧ N ∈ M N ∧ M ≠ N → M ∈ V ∧ N ∈ V ↔ M N ⊆ V
13 12 biimprd ⊢ M ∈ M N ∧ N ∈ M N ∧ M ≠ N → M N ⊆ V → M ∈ V ∧ N ∈ V
14 10 13 syl ⊢ M N = 2 → M N ⊆ V → M ∈ V ∧ N ∈ V
15 14 impcom ⊢ M N ⊆ V ∧ M N = 2 → M ∈ V ∧ N ∈ V
16 8 15 syl6bi ⊢ E ⁡ X = M N → E ⁡ X ⊆ V ∧ E ⁡ X = 2 → M ∈ V ∧ N ∈ V
17 16 com12 ⊢ E ⁡ X ⊆ V ∧ E ⁡ X = 2 → E ⁡ X = M N → M ∈ V ∧ N ∈ V
18 3 4 17 syl2anc ⊢ G ∈ USGraph ∧ X ∈ dom ⁡ E → E ⁡ X = M N → M ∈ V ∧ N ∈ V