usg2spot2nb - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > usg2spot2nb		Structured version Visualization version GIF version

Theorem usg2spot2nb 26592

Description: The set of paths of length 2 with a given vertex in the middle for a finite graph is the union of all paths of length 2 from one neighbor to another neighbor of this vertex via this vertex. (Contributed by Alexander van der Vekens, 9-Mar-2018.)

**Hypothesis**
Ref	Expression
usgreghash2spot.m	⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑡)) = 𝑎)})

**Assertion**
Ref	Expression
usg2spot2nb	⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝑀‘𝑁) = ∪ 𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)∪ 𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥}){⟨𝑥, 𝑁, 𝑦⟩})

Distinct variable groups: 𝑡,𝐸,𝑥,𝑦 𝑁,𝑎,𝑡,𝑥,𝑦 𝑉,𝑎,𝑡,𝑥,𝑦 𝐸,𝑎 Allowed substitution hints: 𝑀(𝑥,𝑦,𝑡,𝑎)

Proof of Theorem usg2spot2nb Dummy variables 𝑚 𝑝 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp3 1056	. . . . 5 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → 𝑁 ∈ 𝑉)
2		3xpexg 6859	. . . . . . 7 ⊢ (𝑉 ∈ Fin → ((𝑉 × 𝑉) × 𝑉) ∈ V)
3		rabexg 4739	. . . . . . 7 ⊢ (((𝑉 × 𝑉) × 𝑉) ∈ V → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑡)) = 𝑁)} ∈ V)
4	2, 3	syl 17	. . . . . 6 ⊢ (𝑉 ∈ Fin → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑡)) = 𝑁)} ∈ V)
5	4	3ad2ant2 1076	. . . . 5 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑡)) = 𝑁)} ∈ V)
6		eqeq2 2621	. . . . . . . . 9 ⊢ (𝑎 = 𝑁 → ((2^nd ‘(1^st ‘𝑡)) = 𝑎 ↔ (2^nd ‘(1^st ‘𝑡)) = 𝑁))
7	6	anbi2d 736	. . . . . . . 8 ⊢ (𝑎 = 𝑁 → ((𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑡)) = 𝑎) ↔ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑡)) = 𝑁)))
8	7	rabbidv 3164	. . . . . . 7 ⊢ (𝑎 = 𝑁 → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑡)) = 𝑎)} = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑡)) = 𝑁)})
9		usgreghash2spot.m	. . . . . . 7 ⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑡)) = 𝑎)})
10	8, 9	fvmptg 6189	. . . . . 6 ⊢ ((𝑁 ∈ 𝑉 ∧ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑡)) = 𝑁)} ∈ V) → (𝑀‘𝑁) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑡)) = 𝑁)})
11	10	eleq2d 2673	. . . . 5 ⊢ ((𝑁 ∈ 𝑉 ∧ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑡)) = 𝑁)} ∈ V) → (𝑧 ∈ (𝑀‘𝑁) ↔ 𝑧 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑡)) = 𝑁)}))
12	1, 5, 11	syl2anc 691	. . . 4 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝑧 ∈ (𝑀‘𝑁) ↔ 𝑧 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑡)) = 𝑁)}))
13		eleq1 2676	. . . . . . . 8 ⊢ (𝑡 = 𝑧 → (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ↔ 𝑧 ∈ (𝑉 2SPathsOt 𝐸)))
14		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑡 = 𝑧 → (1^st ‘𝑡) = (1^st ‘𝑧))
15	14	fveq2d 6107	. . . . . . . . 9 ⊢ (𝑡 = 𝑧 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑧)))
16	15	eqeq1d 2612	. . . . . . . 8 ⊢ (𝑡 = 𝑧 → ((2^nd ‘(1^st ‘𝑡)) = 𝑁 ↔ (2^nd ‘(1^st ‘𝑧)) = 𝑁))
17	13, 16	anbi12d 743	. . . . . . 7 ⊢ (𝑡 = 𝑧 → ((𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑡)) = 𝑁) ↔ (𝑧 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁)))
18	17	elrab 3331	. . . . . 6 ⊢ (𝑧 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑡)) = 𝑁)} ↔ (𝑧 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑧 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁)))
19	18	a1i 11	. . . . 5 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝑧 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑡)) = 𝑁)} ↔ (𝑧 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑧 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁))))
20		usgrav 25867	. . . . . . . . . 10 ⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V))
21		el2spthsoton 26406	. . . . . . . . . 10 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑧 ∈ (𝑉 2SPathsOt 𝐸) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 𝑧 ∈ (𝑥(𝑉 2SPathOnOt 𝐸)𝑦)))
22	20, 21	syl 17	. . . . . . . . 9 ⊢ (𝑉 USGrph 𝐸 → (𝑧 ∈ (𝑉 2SPathsOt 𝐸) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 𝑧 ∈ (𝑥(𝑉 2SPathOnOt 𝐸)𝑦)))
23	22	3ad2ant1 1075	. . . . . . . 8 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝑧 ∈ (𝑉 2SPathsOt 𝐸) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 𝑧 ∈ (𝑥(𝑉 2SPathOnOt 𝐸)𝑦)))
24		usg2spthonot1 26417	. . . . . . . . . 10 ⊢ ((𝑉 USGrph 𝐸 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑧 ∈ (𝑥(𝑉 2SPathOnOt 𝐸)𝑦) ↔ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸))))
25	24	3ad2antl1 1216	. . . . . . . . 9 ⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑧 ∈ (𝑥(𝑉 2SPathOnOt 𝐸)𝑦) ↔ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸))))
26	25	2rexbidva 3038	. . . . . . . 8 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 𝑧 ∈ (𝑥(𝑉 2SPathOnOt 𝐸)𝑦) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸))))
27	23, 26	bitrd 267	. . . . . . 7 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝑧 ∈ (𝑉 2SPathsOt 𝐸) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸))))
28	27	anbi1d 737	. . . . . 6 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((𝑧 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ↔ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁)))
29	28	anbi2d 736	. . . . 5 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((𝑧 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑧 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁)) ↔ (𝑧 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁))))
30		r19.41vv 3072	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)) ↔ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))
31		ancom 465	. . . . . . 7 ⊢ ((∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)) ↔ (𝑧 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁)))
32		r19.41vv 3072	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ↔ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁))
33	32	anbi2i 726	. . . . . . 7 ⊢ ((𝑧 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁)) ↔ (𝑧 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁)))
34	30, 31, 33	3bitrri 286	. . . . . 6 ⊢ ((𝑧 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁)) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))
35		velsn 4141	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩} ↔ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)
36	35	bicomi 213	. . . . . . . . . . . 12 ⊢ (𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ ↔ 𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩})
37	36	anbi2i 726	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) ↔ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩}))
38	37	anbi2i 726	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)) ↔ (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩})))
39	38	a1i 11	. . . . . . . . 9 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)) ↔ (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩}))))
40		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ → (1^st ‘𝑧) = (1^st ‘⟨𝑥, 𝑚, 𝑦⟩))
41	40	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ → (2^nd ‘(1^st ‘𝑧)) = (2^nd ‘(1^st ‘⟨𝑥, 𝑚, 𝑦⟩)))
42		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑥 ∈ V
43		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑚 ∈ V
44		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑦 ∈ V
45		ot2ndg 7074	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 ∈ V ∧ 𝑚 ∈ V ∧ 𝑦 ∈ V) → (2^nd ‘(1^st ‘⟨𝑥, 𝑚, 𝑦⟩)) = 𝑚)
46	42, 43, 44, 45	mp3an 1416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (2^nd ‘(1^st ‘⟨𝑥, 𝑚, 𝑦⟩)) = 𝑚
47	41, 46	syl6eq 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ → (2^nd ‘(1^st ‘𝑧)) = 𝑚)
48	47	eqeq1d 2612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ → ((2^nd ‘(1^st ‘𝑧)) = 𝑁 ↔ 𝑚 = 𝑁))
49		simpr 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((((𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ ∧ ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑁 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) ∧ 𝑁 ∈ 𝑉) → 𝑁 ∈ 𝑉)
50		simplrl 796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((((𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ ∧ ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑁 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) ∧ 𝑁 ∈ 𝑉) → 𝑦 ∈ 𝑉)
51		simplrr 797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ ∧ ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸)) ∧ 𝑥 ≠ 𝑦) → {𝑁, 𝑦} ∈ ran 𝐸)
52	51	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((((𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ ∧ ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑁 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) ∧ 𝑁 ∈ 𝑉) → {𝑁, 𝑦} ∈ ran 𝐸)
53	49, 50, 52	3jca 1235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ ∧ ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑁 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) ∧ 𝑁 ∈ 𝑉) → (𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸))
54		nesym 2838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑦 = 𝑥)
55	54	biimpi 205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑥 ≠ 𝑦 → ¬ 𝑦 = 𝑥)
56	55	ad4antlr 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ ∧ ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑁 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) ∧ 𝑁 ∈ 𝑉) → ¬ 𝑦 = 𝑥)
57	53, 56	jca 553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ ∧ ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑁 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) ∧ 𝑁 ∈ 𝑉) → ((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥))
58		simplrr 797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ ∧ ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑁 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) ∧ 𝑁 ∈ 𝑉) → 𝑥 ∈ 𝑉)
59		prcom 4211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ {𝑥, 𝑁} = {𝑁, 𝑥}
60	59	eleq1i 2679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ({𝑥, 𝑁} ∈ ran 𝐸 ↔ {𝑁, 𝑥} ∈ ran 𝐸)
61	60	biimpi 205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ({𝑥, 𝑁} ∈ ran 𝐸 → {𝑁, 𝑥} ∈ ran 𝐸)
62	61	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸) → {𝑁, 𝑥} ∈ ran 𝐸)
63	62	ad5antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ ∧ ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑁 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) ∧ 𝑁 ∈ 𝑉) → {𝑁, 𝑥} ∈ ran 𝐸)
64	49, 58, 63	3jca 1235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ ∧ ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑁 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) ∧ 𝑁 ∈ 𝑉) → (𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸))
65		simp-5l 804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ ∧ ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑁 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) ∧ 𝑁 ∈ 𝑉) → 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)
66	57, 64, 65	jca32 556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((((𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ ∧ ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑁 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) ∧ 𝑁 ∈ 𝑉) → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)))
67	66	exp31 628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ ∧ ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑁 ∈ 𝑉) → ((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝑁 ∈ 𝑉 → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)))))
68	67	exp41 636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ → (({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸) → (𝑥 ≠ 𝑦 → (𝑁 ∈ 𝑉 → ((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝑁 ∈ 𝑉 → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩))))))))
69	68	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = 𝑁 → (𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ → (({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸) → (𝑥 ≠ 𝑦 → (𝑁 ∈ 𝑉 → ((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝑁 ∈ 𝑉 → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)))))))))
70		oteq2 4350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = 𝑁 → ⟨𝑥, 𝑚, 𝑦⟩ = ⟨𝑥, 𝑁, 𝑦⟩)
71	70	eqeq2d 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = 𝑁 → (𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ↔ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩))
72		preq2 4213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 = 𝑁 → {𝑥, 𝑚} = {𝑥, 𝑁})
73	72	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑚 = 𝑁 → ({𝑥, 𝑚} ∈ ran 𝐸 ↔ {𝑥, 𝑁} ∈ ran 𝐸))
74		preq1 4212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 = 𝑁 → {𝑚, 𝑦} = {𝑁, 𝑦})
75	74	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑚 = 𝑁 → ({𝑚, 𝑦} ∈ ran 𝐸 ↔ {𝑁, 𝑦} ∈ ran 𝐸))
76	73, 75	anbi12d 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = 𝑁 → (({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸) ↔ ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸)))
77		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 = 𝑁 → (𝑚 ∈ 𝑉 ↔ 𝑁 ∈ 𝑉))
78	77	imbi1d 330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑚 = 𝑁 → ((𝑚 ∈ 𝑉 → ((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝑁 ∈ 𝑉 → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩))))) ↔ (𝑁 ∈ 𝑉 → ((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝑁 ∈ 𝑉 → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)))))))
79	78	imbi2d 329	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = 𝑁 → ((𝑥 ≠ 𝑦 → (𝑚 ∈ 𝑉 → ((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝑁 ∈ 𝑉 → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)))))) ↔ (𝑥 ≠ 𝑦 → (𝑁 ∈ 𝑉 → ((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝑁 ∈ 𝑉 → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩))))))))
80	76, 79	imbi12d 333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = 𝑁 → ((({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸) → (𝑥 ≠ 𝑦 → (𝑚 ∈ 𝑉 → ((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝑁 ∈ 𝑉 → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩))))))) ↔ (({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸) → (𝑥 ≠ 𝑦 → (𝑁 ∈ 𝑉 → ((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝑁 ∈ 𝑉 → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)))))))))
81	69, 71, 80	3imtr4d 282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = 𝑁 → (𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ → (({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸) → (𝑥 ≠ 𝑦 → (𝑚 ∈ 𝑉 → ((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝑁 ∈ 𝑉 → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)))))))))
82	81	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ → (𝑚 = 𝑁 → (({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸) → (𝑥 ≠ 𝑦 → (𝑚 ∈ 𝑉 → ((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝑁 ∈ 𝑉 → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)))))))))
83	48, 82	sylbid 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ → ((2^nd ‘(1^st ‘𝑧)) = 𝑁 → (({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸) → (𝑥 ≠ 𝑦 → (𝑚 ∈ 𝑉 → ((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝑁 ∈ 𝑉 → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)))))))))
84	83	com24 93	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ → (𝑥 ≠ 𝑦 → (({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸) → ((2^nd ‘(1^st ‘𝑧)) = 𝑁 → (𝑚 ∈ 𝑉 → ((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝑁 ∈ 𝑉 → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)))))))))
85	84	imp31 447	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) → ((2^nd ‘(1^st ‘𝑧)) = 𝑁 → (𝑚 ∈ 𝑉 → ((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝑁 ∈ 𝑉 → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)))))))
86	85	com14 94	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → ((2^nd ‘(1^st ‘𝑧)) = 𝑁 → (𝑚 ∈ 𝑉 → (((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) → (𝑁 ∈ 𝑉 → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)))))))
87	86	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)) → ((2^nd ‘(1^st ‘𝑧)) = 𝑁 → (𝑚 ∈ 𝑉 → (((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) → (𝑁 ∈ 𝑉 → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)))))))
88	87	imp41 617	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑚 ∈ 𝑉) ∧ ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸))) → (𝑁 ∈ 𝑉 → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩))))
89	88	com12 32	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ 𝑉 → ((((((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑚 ∈ 𝑉) ∧ ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸))) → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩))))
90	89	3ad2ant3 1077	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((((((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑚 ∈ 𝑉) ∧ ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸))) → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩))))
91	90	expdcom 454	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑚 ∈ 𝑉) → (((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)))))
92	91	rexlimdva 3013	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) → (∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)))))
93	92	ex 449	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)) → ((2^nd ‘(1^st ‘𝑧)) = 𝑁 → (∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩))))))
94	93	com13 86	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) → ((2^nd ‘(1^st ‘𝑧)) = 𝑁 → (((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)) → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩))))))
95	94	imp 444	. . . . . . . . . . . . . . . . 17 ⊢ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) → (((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)) → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)))))
96	95	expcomd 453	. . . . . . . . . . . . . . . 16 ⊢ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) → (𝑧 ∈ ((𝑉 × 𝑉) × 𝑉) → ((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩))))))
97	96	imp 444	. . . . . . . . . . . . . . 15 ⊢ (((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)) → ((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)))))
98	97	expdcom 454	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝑉 → (𝑥 ∈ 𝑉 → (((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)) → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩))))))
99	98	com23 84	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝑉 → (((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)) → (𝑥 ∈ 𝑉 → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩))))))
100	99	imp 444	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝑉 ∧ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉))) → (𝑥 ∈ 𝑉 → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)))))
101	100	impcom 445	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))) → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩))))
102	101	com12 32	. . . . . . . . . 10 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))) → (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩))))
103		simprl2 1100	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)) → 𝑥 ∈ 𝑉)
104		simpll2 1094	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)) → 𝑦 ∈ 𝑉)
105		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ 𝑉 → 𝑁 ∈ 𝑉)
106		simpr 476	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((({𝑁, 𝑦} ∈ ran 𝐸 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) → 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)
107	54	bicomi 213	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ 𝑦 = 𝑥 ↔ 𝑥 ≠ 𝑦)
108	107	biimpi 205	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ 𝑦 = 𝑥 → 𝑥 ≠ 𝑦)
109	106, 108	anim12i 588	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((({𝑁, 𝑦} ∈ ran 𝐸 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) ∧ ¬ 𝑦 = 𝑥) → (𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ ∧ 𝑥 ≠ 𝑦))
110		prcom 4211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ {𝑁, 𝑥} = {𝑥, 𝑁}
111	110	eleq1i 2679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ({𝑁, 𝑥} ∈ ran 𝐸 ↔ {𝑥, 𝑁} ∈ ran 𝐸)
112	111	biimpi 205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ({𝑁, 𝑥} ∈ ran 𝐸 → {𝑥, 𝑁} ∈ ran 𝐸)
113	112	anim1i 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({𝑁, 𝑥} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸) → ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸))
114	113	ancoms 468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (({𝑁, 𝑦} ∈ ran 𝐸 ∧ {𝑁, 𝑥} ∈ ran 𝐸) → ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸))
115	114	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((({𝑁, 𝑦} ∈ ran 𝐸 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) → ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸))
116	115	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((({𝑁, 𝑦} ∈ ran 𝐸 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) ∧ ¬ 𝑦 = 𝑥) → ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸))
117	109, 116	jca 553	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((({𝑁, 𝑦} ∈ ran 𝐸 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) ∧ ¬ 𝑦 = 𝑥) → ((𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸)))
118	71	anbi1d 737	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 = 𝑁 → ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ↔ (𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ ∧ 𝑥 ≠ 𝑦)))
119	118, 76	anbi12d 743	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = 𝑁 → (((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ↔ ((𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑁} ∈ ran 𝐸 ∧ {𝑁, 𝑦} ∈ ran 𝐸))))
120	117, 119	syl5ibr 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = 𝑁 → (((({𝑁, 𝑦} ∈ ran 𝐸 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) ∧ ¬ 𝑦 = 𝑥) → ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸))))
121	120	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑚 = 𝑁) → (((({𝑁, 𝑦} ∈ ran 𝐸 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) ∧ ¬ 𝑦 = 𝑥) → ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸))))
122	105, 121	rspcimedv 3284	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ 𝑉 → (((({𝑁, 𝑦} ∈ ran 𝐸 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) ∧ ¬ 𝑦 = 𝑥) → ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸))))
123	122	expdcom 454	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((({𝑁, 𝑦} ∈ ran 𝐸 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) → (¬ 𝑦 = 𝑥 → (𝑁 ∈ 𝑉 → ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)))))
124	123	exp31 628	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑁, 𝑦} ∈ ran 𝐸 → ({𝑁, 𝑥} ∈ ran 𝐸 → (𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ → (¬ 𝑦 = 𝑥 → (𝑁 ∈ 𝑉 → ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)))))))
125	124	com15 99	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ 𝑉 → ({𝑁, 𝑥} ∈ ran 𝐸 → (𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ → (¬ 𝑦 = 𝑥 → ({𝑁, 𝑦} ∈ ran 𝐸 → ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)))))))
126	125	imp 444	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) → (𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ → (¬ 𝑦 = 𝑥 → ({𝑁, 𝑦} ∈ ran 𝐸 → ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸))))))
127	126	3adant2 1073	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) → (𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ → (¬ 𝑦 = 𝑥 → ({𝑁, 𝑦} ∈ ran 𝐸 → ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸))))))
128	127	imp 444	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) → (¬ 𝑦 = 𝑥 → ({𝑁, 𝑦} ∈ ran 𝐸 → ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)))))
129	128	com13 86	. . . . . . . . . . . . . 14 ⊢ ({𝑁, 𝑦} ∈ ran 𝐸 → (¬ 𝑦 = 𝑥 → (((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) → ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)))))
130	129	3ad2ant3 1077	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) → (¬ 𝑦 = 𝑥 → (((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) → ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)))))
131	130	imp31 447	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)) → ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)))
132		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ → (1^st ‘𝑧) = (1^st ‘⟨𝑥, 𝑁, 𝑦⟩))
133	132	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ → (2^nd ‘(1^st ‘𝑧)) = (2^nd ‘(1^st ‘⟨𝑥, 𝑁, 𝑦⟩)))
134		simpl 472	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ 𝑉 ∧ (𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝑥 ∈ 𝑉)
135		simprl 790	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ 𝑉 ∧ (𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝑁 ∈ 𝑉)
136		simprr 792	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ 𝑉 ∧ (𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝑦 ∈ 𝑉)
137	134, 135, 136	3jca 1235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ 𝑉 ∧ (𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉))
138		ot2ndg 7074	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (2^nd ‘(1^st ‘⟨𝑥, 𝑁, 𝑦⟩)) = 𝑁)
139	137, 138	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ 𝑉 ∧ (𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (2^nd ‘(1^st ‘⟨𝑥, 𝑁, 𝑦⟩)) = 𝑁)
140	133, 139	sylan9eqr 2666	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ 𝑉 ∧ (𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) → (2^nd ‘(1^st ‘𝑧)) = 𝑁)
141	140	exp31 628	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑉 → ((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ → (2^nd ‘(1^st ‘𝑧)) = 𝑁)))
142	141	com23 84	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝑉 → (𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ → ((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (2^nd ‘(1^st ‘𝑧)) = 𝑁)))
143	142	3ad2ant2 1076	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) → (𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ → ((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (2^nd ‘(1^st ‘𝑧)) = 𝑁)))
144	143	imp 444	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) → ((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (2^nd ‘(1^st ‘𝑧)) = 𝑁))
145	144	com12 32	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) → (2^nd ‘(1^st ‘𝑧)) = 𝑁))
146	145	3adant3 1074	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) → (((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) → (2^nd ‘(1^st ‘𝑧)) = 𝑁))
147	146	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) → (((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) → (2^nd ‘(1^st ‘𝑧)) = 𝑁))
148	147	imp 444	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)) → (2^nd ‘(1^st ‘𝑧)) = 𝑁)
149		eqidd 2611	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ 𝑉 ∧ (𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ⟨𝑥, 𝑁, 𝑦⟩ = ⟨𝑥, 𝑁, 𝑦⟩)
150		otel3xp 5077	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((⟨𝑥, 𝑁, 𝑦⟩ = ⟨𝑥, 𝑁, 𝑦⟩ ∧ (𝑥 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ⟨𝑥, 𝑁, 𝑦⟩ ∈ ((𝑉 × 𝑉) × 𝑉))
151	149, 137, 150	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ 𝑉 ∧ (𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ⟨𝑥, 𝑁, 𝑦⟩ ∈ ((𝑉 × 𝑉) × 𝑉))
152	151	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝑉 ∧ (𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) → ⟨𝑥, 𝑁, 𝑦⟩ ∈ ((𝑉 × 𝑉) × 𝑉))
153		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ → (𝑧 ∈ ((𝑉 × 𝑉) × 𝑉) ↔ ⟨𝑥, 𝑁, 𝑦⟩ ∈ ((𝑉 × 𝑉) × 𝑉)))
154	153	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ 𝑉 ∧ (𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) → (𝑧 ∈ ((𝑉 × 𝑉) × 𝑉) ↔ ⟨𝑥, 𝑁, 𝑦⟩ ∈ ((𝑉 × 𝑉) × 𝑉)))
155	152, 154	mpbird 246	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ 𝑉 ∧ (𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) → 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉))
156	155	exp31 628	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑉 → ((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ → 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉))))
157	156	com23 84	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝑉 → (𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ → ((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉))))
158	157	3ad2ant2 1076	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) → (𝑧 = ⟨𝑥, 𝑁, 𝑦⟩ → ((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉))))
159	158	imp 444	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) → ((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))
160	159	com12 32	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) → 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))
161	160	3adant3 1074	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) → (((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) → 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))
162	161	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) → (((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩) → 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))
163	162	imp 444	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)) → 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉))
164	131, 148, 163	jca31 555	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)) → ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))
165	103, 104, 164	jca32 556	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩)) → (𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))))
166	102, 165	impbid1 214	. . . . . . . . 9 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))) ↔ (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 = ⟨𝑥, 𝑁, 𝑦⟩))))
167		eldif 3550	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥}) ↔ (𝑦 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∧ ¬ 𝑦 ∈ {𝑥}))
168		nbgrael 25955	. . . . . . . . . . . . . 14 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑦 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ↔ (𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸)))
169	20, 168	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑉 USGrph 𝐸 → (𝑦 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ↔ (𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸)))
170	169	3ad2ant1 1075	. . . . . . . . . . . 12 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝑦 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ↔ (𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸)))
171		velsn 4141	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
172	171	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥))
173	172	notbid 307	. . . . . . . . . . . 12 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (¬ 𝑦 ∈ {𝑥} ↔ ¬ 𝑦 = 𝑥))
174	170, 173	anbi12d 743	. . . . . . . . . . 11 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((𝑦 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∧ ¬ 𝑦 ∈ {𝑥}) ↔ ((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥)))
175	167, 174	syl5bb 271	. . . . . . . . . 10 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥}) ↔ ((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥)))
176		nbgrael 25955	. . . . . . . . . . . . 13 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ↔ (𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸)))
177	20, 176	syl 17	. . . . . . . . . . . 12 ⊢ (𝑉 USGrph 𝐸 → (𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ↔ (𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸)))
178	177	3ad2ant1 1075	. . . . . . . . . . 11 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ↔ (𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸)))
179	178	anbi1d 737	. . . . . . . . . 10 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∧ 𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩}) ↔ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩})))
180	175, 179	anbi12d 743	. . . . . . . . 9 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∧ 𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩})) ↔ (((𝑁 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ {𝑁, 𝑦} ∈ ran 𝐸) ∧ ¬ 𝑦 = 𝑥) ∧ ((𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ {𝑁, 𝑥} ∈ ran 𝐸) ∧ 𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩}))))
181	39, 166, 180	3bitr4d 299	. . . . . . . 8 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))) ↔ (𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∧ 𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩}))))
182	181	2exbidv 1839	. . . . . . 7 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (∃𝑥∃𝑦(𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))) ↔ ∃𝑥∃𝑦(𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∧ 𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩}))))
183		df-rex 2902	. . . . . . . . 9 ⊢ (∃𝑦 ∈ 𝑉 ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)) ↔ ∃𝑦(𝑦 ∈ 𝑉 ∧ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉))))
184	183	rexbii 3023	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦(𝑦 ∈ 𝑉 ∧ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉))))
185		df-rex 2902	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝑉 ∃𝑦(𝑦 ∈ 𝑉 ∧ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉))) ↔ ∃𝑥(𝑥 ∈ 𝑉 ∧ ∃𝑦(𝑦 ∈ 𝑉 ∧ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))))
186		19.42v 1905	. . . . . . . . . 10 ⊢ (∃𝑦(𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))) ↔ (𝑥 ∈ 𝑉 ∧ ∃𝑦(𝑦 ∈ 𝑉 ∧ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))))
187	186	bicomi 213	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝑉 ∧ ∃𝑦(𝑦 ∈ 𝑉 ∧ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))) ↔ ∃𝑦(𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))))
188	187	exbii 1764	. . . . . . . 8 ⊢ (∃𝑥(𝑥 ∈ 𝑉 ∧ ∃𝑦(𝑦 ∈ 𝑉 ∧ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))))
189	184, 185, 188	3bitri 285	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)))))
190		df-rex 2902	. . . . . . . 8 ⊢ (∃𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩} ↔ ∃𝑥(𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∧ ∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩}))
191		r19.42v 3073	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})(𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∧ 𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩}) ↔ (𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∧ ∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩}))
192		df-rex 2902	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})(𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∧ 𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩}) ↔ ∃𝑦(𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∧ 𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩})))
193	191, 192	bitr3i 265	. . . . . . . . 9 ⊢ ((𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∧ ∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩}) ↔ ∃𝑦(𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∧ 𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩})))
194	193	exbii 1764	. . . . . . . 8 ⊢ (∃𝑥(𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∧ ∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩}) ↔ ∃𝑥∃𝑦(𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∧ 𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩})))
195	190, 194	bitri 263	. . . . . . 7 ⊢ (∃𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩} ↔ ∃𝑥∃𝑦(𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∧ 𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩})))
196	182, 189, 195	3bitr4g 302	. . . . . 6 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ((∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁) ∧ 𝑧 ∈ ((𝑉 × 𝑉) × 𝑉)) ↔ ∃𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩}))
197	34, 196	syl5bb 271	. . . . 5 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((𝑧 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨𝑥, 𝑚, 𝑦⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑦} ∈ ran 𝐸)) ∧ (2^nd ‘(1^st ‘𝑧)) = 𝑁)) ↔ ∃𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩}))
198	19, 29, 197	3bitrd 293	. . . 4 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝑧 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2^nd ‘(1^st ‘𝑡)) = 𝑁)} ↔ ∃𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩}))
199		vex 3176	. . . . . . 7 ⊢ 𝑧 ∈ V
200		eleq1 2676	. . . . . . . 8 ⊢ (𝑝 = 𝑧 → (𝑝 ∈ {⟨𝑥, 𝑁, 𝑦⟩} ↔ 𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩}))
201	200	2rexbidv 3039	. . . . . . 7 ⊢ (𝑝 = 𝑧 → (∃𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑝 ∈ {⟨𝑥, 𝑁, 𝑦⟩} ↔ ∃𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩}))
202	199, 201	elab 3319	. . . . . 6 ⊢ (𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑝 ∈ {⟨𝑥, 𝑁, 𝑦⟩}} ↔ ∃𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩})
203	202	bicomi 213	. . . . 5 ⊢ (∃𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩} ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑝 ∈ {⟨𝑥, 𝑁, 𝑦⟩}})
204	203	a1i 11	. . . 4 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (∃𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑧 ∈ {⟨𝑥, 𝑁, 𝑦⟩} ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑝 ∈ {⟨𝑥, 𝑁, 𝑦⟩}}))
205	12, 198, 204	3bitrd 293	. . 3 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝑧 ∈ (𝑀‘𝑁) ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑝 ∈ {⟨𝑥, 𝑁, 𝑦⟩}}))
206	205	eqrdv 2608	. 2 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝑀‘𝑁) = {𝑝 ∣ ∃𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑝 ∈ {⟨𝑥, 𝑁, 𝑦⟩}})
207		dfiunv2 4492	. 2 ⊢ ∪ 𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)∪ 𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥}){⟨𝑥, 𝑁, 𝑦⟩} = {𝑝 ∣ ∃𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)∃𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥})𝑝 ∈ {⟨𝑥, 𝑁, 𝑦⟩}}
208	206, 207	syl6eqr 2662	1 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝑀‘𝑁) = ∪ 𝑥 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝑁)∪ 𝑦 ∈ ((⟨𝑉, 𝐸⟩ Neighbors 𝑁) ∖ {𝑥}){⟨𝑥, 𝑁, 𝑦⟩})

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∃wex 1695 ∈ wcel 1977 {cab 2596 ≠ wne 2780 ∃wrex 2897 {crab 2900 Vcvv 3173 ∖ cdif 3537 {csn 4125 {cpr 4127 ⟨cop 4131 ⟨cotp 4133 ∪ ciun 4455 class class class wbr 4583 ↦ cmpt 4643 × cxp 5036 ran crn 5039 ‘cfv 5804 (class class class)co 6549 1^st c1st 7057 2^nd c2nd 7058 Fincfn 7841 USGrph cusg 25859 Neighbors cnbgra 25946 2SPathsOt c2spthot 26383 2SPathOnOt c2pthonot 26384

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-ot 4134 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-map 7746 df-pm 7747 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-2 10956 df-n0 11170 df-z 11255 df-uz 11564 df-fz 12198 df-fzo 12335 df-hash 12980 df-word 13154 df-usgra 25862 df-nbgra 25949 df-wlk 26036 df-trail 26037 df-pth 26038 df-spth 26039 df-wlkon 26042 df-spthon 26045 df-2wlkonot 26385 df-2spthonot 26387 df-2spthsot 26388

This theorem is referenced by: usgreghash2spotv 26593

W3C validator