2spthonot3v - Metamath Proof Explorer

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

Theorem 2spthonot3v 26403

Description: If an ordered triple represents a simple path of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.)

**Assertion**
Ref	Expression
2spthonot3v	⊢ (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))

Proof of Theorem 2spthonot3v Dummy variables 𝑓 𝑝 𝑡 𝑎 𝑏 𝑐 𝑒 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ne0i 3880	. . 3 ⊢ (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) ≠ ∅)
2		df-ov 6552	. . . . 5 ⊢ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) = ((𝑉 2SPathOnOt 𝐸)‘⟨𝐴, 𝐶⟩)
3		ndmfv 6128	. . . . 5 ⊢ (¬ ⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → ((𝑉 2SPathOnOt 𝐸)‘⟨𝐴, 𝐶⟩) = ∅)
4	2, 3	syl5eq 2656	. . . 4 ⊢ (¬ ⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) = ∅)
5	4	necon1ai 2809	. . 3 ⊢ ((𝐴(𝑉 2SPathOnOt 𝐸)𝐶) ≠ ∅ → ⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸))
6		simpl 472	. . . . . . . . 9 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → 𝑣 = 𝑉)
7		id 22	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑉 → 𝑣 = 𝑉)
8	7, 7	xpeq12d 5064	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑉 → (𝑣 × 𝑣) = (𝑉 × 𝑉))
9	8, 7	xpeq12d 5064	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑉 → ((𝑣 × 𝑣) × 𝑣) = ((𝑉 × 𝑉) × 𝑉))
10	9	adantr 480	. . . . . . . . . 10 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → ((𝑣 × 𝑣) × 𝑣) = ((𝑉 × 𝑉) × 𝑉))
11		oveq12 6558	. . . . . . . . . . . . . 14 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑣 SPathOn 𝑒) = (𝑉 SPathOn 𝐸))
12	11	oveqd 6566	. . . . . . . . . . . . 13 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑎(𝑣 SPathOn 𝑒)𝑏) = (𝑎(𝑉 SPathOn 𝐸)𝑏))
13	12	breqd 4594	. . . . . . . . . . . 12 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ↔ 𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝))
14	13	3anbi1d 1395	. . . . . . . . . . 11 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → ((𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏)) ↔ (𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))))
15	14	2exbidv 1839	. . . . . . . . . 10 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (∃𝑓∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏)) ↔ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))))
16	10, 15	rabeqbidv 3168	. . . . . . . . 9 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))} = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))})
17	6, 6, 16	mpt2eq123dv 6615	. . . . . . . 8 ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}))
18		df-2spthonot 26387	. . . . . . . 8 ⊢ 2SPathOnOt = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}))
19	17, 18	ovmpt2ga 6688	. . . . . . 7 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V) → (𝑉 2SPathOnOt 𝐸) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}))
20	19	dmeqd 5248	. . . . . 6 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V) → dom (𝑉 2SPathOnOt 𝐸) = dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}))
21	20	eleq2d 2673	. . . . 5 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) ↔ ⟨𝐴, 𝐶⟩ ∈ dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))})))
22		dmoprabss 6640	. . . . . . . . 9 ⊢ dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))})} ⊆ (𝑉 × 𝑉)
23	22	sseli 3564	. . . . . . . 8 ⊢ (⟨𝐴, 𝐶⟩ ∈ dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))})} → ⟨𝐴, 𝐶⟩ ∈ (𝑉 × 𝑉))
24		opelxp 5070	. . . . . . . . . . . 12 ⊢ (⟨𝐴, 𝐶⟩ ∈ (𝑉 × 𝑉) ↔ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))
25		2spthonot 26393	. . . . . . . . . . . . . . 15 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝐴 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝐶))})
26	25	eleq2d 2673	. . . . . . . . . . . . . 14 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) ↔ 𝑇 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝐴 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝐶))}))
27		elrabi 3328	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝐴 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝐶))} → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))
28		simpl 472	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑉 ∈ V ∧ 𝐸 ∈ V))
29	28	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)) → (𝑉 ∈ V ∧ 𝐸 ∈ V))
30		simpr 476	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))
31	30	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)) → (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))
32		simpr 476	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))
33	29, 31, 32	3jca 1235	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))
34	33	ex 449	. . . . . . . . . . . . . . 15 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))))
35	27, 34	syl5 33	. . . . . . . . . . . . . 14 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑇 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝐴 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝐶))} → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))))
36	26, 35	sylbid 229	. . . . . . . . . . . . 13 ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))))
37	36	expcom 450	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
38	24, 37	sylbi 206	. . . . . . . . . . 11 ⊢ (⟨𝐴, 𝐶⟩ ∈ (𝑉 × 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
39	38	com12 32	. . . . . . . . . 10 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (⟨𝐴, 𝐶⟩ ∈ (𝑉 × 𝑉) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
40	39	3adant3 1074	. . . . . . . . 9 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V) → (⟨𝐴, 𝐶⟩ ∈ (𝑉 × 𝑉) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
41	40	com12 32	. . . . . . . 8 ⊢ (⟨𝐴, 𝐶⟩ ∈ (𝑉 × 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
42	23, 41	syl 17	. . . . . . 7 ⊢ (⟨𝐴, 𝐶⟩ ∈ dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))})} → ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
43		df-mpt2 6554	. . . . . . . 8 ⊢ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) = {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))})}
44	43	dmeqi 5247	. . . . . . 7 ⊢ dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) = dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))})}
45	42, 44	eleq2s 2706	. . . . . 6 ⊢ (⟨𝐴, 𝐶⟩ ∈ dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) → ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
46	45	com12 32	. . . . 5 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
47	21, 46	sylbid 229	. . . 4 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
48		3ianor 1048	. . . . 5 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V) ↔ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V))
49		df-3or 1032	. . . . . 6 ⊢ ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V) ↔ ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V))
50		ianor 508	. . . . . . . 8 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) ↔ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V))
51	18	mpt2ndm0 6773	. . . . . . . . . . . 12 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 2SPathOnOt 𝐸) = ∅)
52	51	dmeqd 5248	. . . . . . . . . . 11 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → dom (𝑉 2SPathOnOt 𝐸) = dom ∅)
53	52	eleq2d 2673	. . . . . . . . . 10 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) ↔ ⟨𝐴, 𝐶⟩ ∈ dom ∅))
54		dm0 5260	. . . . . . . . . . 11 ⊢ dom ∅ = ∅
55	54	eleq2i 2680	. . . . . . . . . 10 ⊢ (⟨𝐴, 𝐶⟩ ∈ dom ∅ ↔ ⟨𝐴, 𝐶⟩ ∈ ∅)
56	53, 55	syl6bb 275	. . . . . . . . 9 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) ↔ ⟨𝐴, 𝐶⟩ ∈ ∅))
57		noel 3878	. . . . . . . . . 10 ⊢ ¬ ⟨𝐴, 𝐶⟩ ∈ ∅
58	57	pm2.21i 115	. . . . . . . . 9 ⊢ (⟨𝐴, 𝐶⟩ ∈ ∅ → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))))
59	56, 58	syl6bi 242	. . . . . . . 8 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
60	50, 59	sylbir 224	. . . . . . 7 ⊢ ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
61		anor 509	. . . . . . . . 9 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ↔ ¬ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V))
62		id 22	. . . . . . . . . . . . 13 ⊢ (𝑉 ∈ V → 𝑉 ∈ V)
63	62	ancri 573	. . . . . . . . . . . 12 ⊢ (𝑉 ∈ V → (𝑉 ∈ V ∧ 𝑉 ∈ V))
64	63	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ∈ V ∧ 𝑉 ∈ V))
65		mpt2exga 7135	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ V ∧ 𝑉 ∈ V) → (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V)
66	64, 65	syl 17	. . . . . . . . . 10 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V)
67	66	pm2.24d 146	. . . . . . . . 9 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))))))
68	61, 67	sylbir 224	. . . . . . . 8 ⊢ (¬ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) → (¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))))))
69	68	imp 444	. . . . . . 7 ⊢ ((¬ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) ∧ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
70	60, 69	jaoi3 1003	. . . . . 6 ⊢ (((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
71	49, 70	sylbi 206	. . . . 5 ⊢ ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
72	48, 71	sylbi 206	. . . 4 ⊢ (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1^st ‘(1^st ‘𝑡)) = 𝑎 ∧ (2^nd ‘(1^st ‘𝑡)) = (𝑝‘1) ∧ (2^nd ‘𝑡) = 𝑏))}) ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
73	47, 72	pm2.61i 175	. . 3 ⊢ (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))))
74	1, 5, 73	3syl 18	. 2 ⊢ (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))))
75	74	pm2.43i 50	1 ⊢ (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∨ wo 382 ∧ wa 383 ∨ w3o 1030 ∧ w3a 1031 = wceq 1475 ∃wex 1695 ∈ wcel 1977 ≠ wne 2780 {crab 2900 Vcvv 3173 ∅c0 3874 ⟨cop 4131 class class class wbr 4583 × cxp 5036 dom cdm 5038 ‘cfv 5804 (class class class)co 6549 {coprab 6550 ↦ cmpt2 6551 1^st c1st 7057 2^nd c2nd 7058 1c1 9816 2c2 10947 #chash 12979 SPathOn cspthon 26033 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

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-ral 2901 df-rex 2902 df-reu 2903 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-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 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-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-1st 7059 df-2nd 7060 df-2spthonot 26387

This theorem is referenced by: el2spthsoton 26406 2spontn0vne 26414 2spot0 26591

W3C validator