usgrnloopvALT

Description: Alternate proof of usgrnloopv , not using umgrnloopv . (Contributed by Alexander van der Vekens, 26-Jan-2018) (Revised by AV, 17-Oct-2020) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Hypothesis	usgrnloopv.e	$⊢ E = iEdg (G)$
	Assertion	usgrnloopvALT	$⊢ (G \in USGraph \land M \in W) \to (E (X) = \{M, N\} \to M \neq N)$

Proof

Step	Hyp	Ref	Expression
1		usgrnloopv.e	$⊢ E = iEdg (G)$
2		prnzg	$⊢ M \in W \to \{M, N\} \neq \emptyset$
3	2	adantl	$⊢ (E (X) = \{M, N\} \land M \in W) \to \{M, N\} \neq \emptyset$
4		neeq1	$⊢ E (X) = \{M, N\} \to (E (X) \neq \emptyset \leftrightarrow \{M, N\} \neq \emptyset)$
5	4	adantr	$⊢ (E (X) = \{M, N\} \land M \in W) \to (E (X) \neq \emptyset \leftrightarrow \{M, N\} \neq \emptyset)$
6	3 5	mpbird	$⊢ (E (X) = \{M, N\} \land M \in W) \to E (X) \neq \emptyset$
7		fvfundmfvn0	$⊢ E (X) \neq \emptyset \to (X \in dom E \land Fun ({E ↾}_{\{X\}}))$
8	6 7	syl	$⊢ (E (X) = \{M, N\} \land M \in W) \to (X \in dom E \land Fun ({E ↾}_{\{X\}}))$
9	1	usgredg2	$⊢ (G \in USGraph \land X \in dom E) \to \|E (X)\| = 2$
10		fveq2	$⊢ E (X) = \{M, N\} \to \|E (X)\| = \|\{M, N\}\|$
11	10	eqeq1d	$⊢ E (X) = \{M, N\} \to (\|E (X)\| = 2 \leftrightarrow \|\{M, N\}\| = 2)$
12		eqid	$⊢ \{M, N\} = \{M, N\}$
13	12	hashprdifel	$⊢ \|\{M, N\}\| = 2 \to (M \in \{M, N\} \land N \in \{M, N\} \land M \neq N)$
14	13	simp3d	$⊢ \|\{M, N\}\| = 2 \to M \neq N$
15	11 14	syl6bi	$⊢ E (X) = \{M, N\} \to (\|E (X)\| = 2 \to M \neq N)$
16	15	adantr	$⊢ (E (X) = \{M, N\} \land M \in W) \to (\|E (X)\| = 2 \to M \neq N)$
17	9 16	syl5com	$⊢ (G \in USGraph \land X \in dom E) \to ((E (X) = \{M, N\} \land M \in W) \to M \neq N)$
18	17	expcom	$⊢ X \in dom E \to (G \in USGraph \to ((E (X) = \{M, N\} \land M \in W) \to M \neq N))$
19	18	com23	$⊢ X \in dom E \to ((E (X) = \{M, N\} \land M \in W) \to (G \in USGraph \to M \neq N))$
20	19	adantr	$⊢ (X \in dom E \land Fun ({E ↾}_{\{X\}})) \to ((E (X) = \{M, N\} \land M \in W) \to (G \in USGraph \to M \neq N))$
21	8 20	mpcom	$⊢ (E (X) = \{M, N\} \land M \in W) \to (G \in USGraph \to M \neq N)$
22	21	ex	$⊢ E (X) = \{M, N\} \to (M \in W \to (G \in USGraph \to M \neq N))$
23	22	com13	$⊢ G \in USGraph \to (M \in W \to (E (X) = \{M, N\} \to M \neq N))$
24	23	imp	$⊢ (G \in USGraph \land M \in W) \to (E (X) = \{M, N\} \to M \neq N)$

Metamath Proof Explorer

Theorem usgrnloopvALT

Proof