Theorem 2spotdisj 26588

Description: All simple paths of length 2 as ordered triple from a fixed vertex to another vertex are disjunct. (Contributed by Alexander van der Vekens, 4-Mar-2018.)

Assertion

Ref	Expression
2spotdisj	⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) → Disj 𝑏 ∈ (𝑉 ∖ {𝐴})(𝐴(𝑉 2SPathOnOt 𝐸)𝑏))

Distinct variable groups:   𝐴,𝑏   𝐸,𝑏   𝑉,𝑏   𝑋,𝑏   𝑌,𝑏

Proof of Theorem 2spotdisj

Dummy variables 𝑐 𝑓 𝑔 𝑝 𝑞 𝑠 𝑡 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		orc 399	. . . . . . . . . 10 ⊢ (𝑏 = 𝑐 → (𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅))
2	1	a1d 25	. . . . . . . . 9 ⊢ (𝑏 = 𝑐 → (((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴}) → (𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅)))
3		2spthonot 26393	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝐴(𝑉 2SPathOnOt 𝐸)𝑏) = {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑠)) = 𝐴 ∧ (2nd ‘(1st ‘𝑠)) = (𝑞‘1) ∧ (2nd ‘𝑠) = 𝑏))})
4	3	anassrs 678	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) → (𝐴(𝑉 2SPathOnOt 𝐸)𝑏) = {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑠)) = 𝐴 ∧ (2nd ‘(1st ‘𝑠)) = (𝑞‘1) ∧ (2nd ‘𝑠) = 𝑏))})
5	4	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) → (𝐴(𝑉 2SPathOnOt 𝐸)𝑏) = {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑠)) = 𝐴 ∧ (2nd ‘(1st ‘𝑠)) = (𝑞‘1) ∧ (2nd ‘𝑠) = 𝑏))})
6		2spthonot 26393	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝐴(𝑉 2SPathOnOt 𝐸)𝑐) = {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑢)) = 𝐴 ∧ (2nd ‘(1st ‘𝑢)) = (𝑝‘1) ∧ (2nd ‘𝑢) = 𝑐))})
7	6	anassrs 678	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) → (𝐴(𝑉 2SPathOnOt 𝐸)𝑐) = {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑢)) = 𝐴 ∧ (2nd ‘(1st ‘𝑢)) = (𝑝‘1) ∧ (2nd ‘𝑢) = 𝑐))})
8	7	adantlr 747	. . . . . . . . . . . . . . 15 ⊢ (((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) → (𝐴(𝑉 2SPathOnOt 𝐸)𝑐) = {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑢)) = 𝐴 ∧ (2nd ‘(1st ‘𝑢)) = (𝑝‘1) ∧ (2nd ‘𝑢) = 𝑐))})
9	5, 8	ineq12d 3777	. . . . . . . . . . . . . 14 ⊢ (((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑐 ∈ 𝑉) → ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ({𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑠)) = 𝐴 ∧ (2nd ‘(1st ‘𝑠)) = (𝑞‘1) ∧ (2nd ‘𝑠) = 𝑏))} ∩ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑢)) = 𝐴 ∧ (2nd ‘(1st ‘𝑢)) = (𝑝‘1) ∧ (2nd ‘𝑢) = 𝑐))}))
10	9	adantlr 747	. . . . . . . . . . . . 13 ⊢ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) → ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ({𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑠)) = 𝐴 ∧ (2nd ‘(1st ‘𝑠)) = (𝑞‘1) ∧ (2nd ‘𝑠) = 𝑏))} ∩ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑢)) = 𝐴 ∧ (2nd ‘(1st ‘𝑢)) = (𝑝‘1) ∧ (2nd ‘𝑢) = 𝑐))}))
11	10	ad2antrl 760	. . . . . . . . . . . 12 ⊢ ((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) → ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ({𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑠)) = 𝐴 ∧ (2nd ‘(1st ‘𝑠)) = (𝑞‘1) ∧ (2nd ‘𝑠) = 𝑏))} ∩ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑢)) = 𝐴 ∧ (2nd ‘(1st ‘𝑢)) = (𝑝‘1) ∧ (2nd ‘𝑢) = 𝑐))}))
12		eqtr2 2630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((2nd ‘𝑡) = 𝑏 ∧ (2nd ‘𝑡) = 𝑐) → 𝑏 = 𝑐)
13	12	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((2nd ‘𝑡) = 𝑏 → ((2nd ‘𝑡) = 𝑐 → 𝑏 = 𝑐))
14	13	con3rr3 150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (¬ 𝑏 = 𝑐 → ((2nd ‘𝑡) = 𝑏 → ¬ (2nd ‘𝑡) = 𝑐))
15	14	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) → ((2nd ‘𝑡) = 𝑏 → ¬ (2nd ‘𝑡) = 𝑐))
16	15	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) → ((2nd ‘𝑡) = 𝑏 → ¬ (2nd ‘𝑡) = 𝑐))
17	16	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2nd ‘𝑡) = 𝑏 → (((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) → ¬ (2nd ‘𝑡) = 𝑐))
18	17	3ad2ant3 1077	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑞‘1) ∧ (2nd ‘𝑡) = 𝑏) → (((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) → ¬ (2nd ‘𝑡) = 𝑐))
19	18	3ad2ant3 1077	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑞‘1) ∧ (2nd ‘𝑡) = 𝑏)) → (((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) → ¬ (2nd ‘𝑡) = 𝑐))
20	19	impcom 445	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ (𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑞‘1) ∧ (2nd ‘𝑡) = 𝑏))) → ¬ (2nd ‘𝑡) = 𝑐)
21	20	intn3an3d 1436	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ (𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑞‘1) ∧ (2nd ‘𝑡) = 𝑏))) → ¬ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐))
22	21	3mix3d 1231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ (𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑞‘1) ∧ (2nd ‘𝑡) = 𝑏))) → (¬ 𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∨ ¬ (#‘𝑓) = 2 ∨ ¬ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐)))
23	22	ex 449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) → ((𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑞‘1) ∧ (2nd ‘𝑡) = 𝑏)) → (¬ 𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∨ ¬ (#‘𝑓) = 2 ∨ ¬ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐))))
24	23	exlimdvv 1849	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) → (∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑞‘1) ∧ (2nd ‘𝑡) = 𝑏)) → (¬ 𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∨ ¬ (#‘𝑓) = 2 ∨ ¬ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐))))
25	24	imp 444	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ ∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑞‘1) ∧ (2nd ‘𝑡) = 𝑏))) → (¬ 𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∨ ¬ (#‘𝑓) = 2 ∨ ¬ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐)))
26	25	alrimivv 1843	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ ∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑞‘1) ∧ (2nd ‘𝑡) = 𝑏))) → ∀𝑓∀𝑝(¬ 𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∨ ¬ (#‘𝑓) = 2 ∨ ¬ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐)))
27		2nexaln 1747	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐)) ↔ ∀𝑓∀𝑝 ¬ (𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐)))
28		3ianor 1048	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐)) ↔ (¬ 𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∨ ¬ (#‘𝑓) = 2 ∨ ¬ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐)))
29	28	bicomi 213	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ 𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∨ ¬ (#‘𝑓) = 2 ∨ ¬ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐)) ↔ ¬ (𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐)))
30	29	2albii 1738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑓∀𝑝(¬ 𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∨ ¬ (#‘𝑓) = 2 ∨ ¬ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐)) ↔ ∀𝑓∀𝑝 ¬ (𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐)))
31	27, 30	bitr4i 266	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐)) ↔ ∀𝑓∀𝑝(¬ 𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∨ ¬ (#‘𝑓) = 2 ∨ ¬ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐)))
32	26, 31	sylibr 223	. . . . . . . . . . . . . . . . . 18 ⊢ ((((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ ∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑞‘1) ∧ (2nd ‘𝑡) = 𝑏))) → ¬ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐)))
33	32	intnand 953	. . . . . . . . . . . . . . . . 17 ⊢ ((((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ ∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑞‘1) ∧ (2nd ‘𝑡) = 𝑏))) → ¬ (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐))))
34		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑡 → (1st ‘𝑢) = (1st ‘𝑡))
35	34	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑡 → (1st ‘(1st ‘𝑢)) = (1st ‘(1st ‘𝑡)))
36	35	eqeq1d 2612	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑡 → ((1st ‘(1st ‘𝑢)) = 𝐴 ↔ (1st ‘(1st ‘𝑡)) = 𝐴))
37	34	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑡 → (2nd ‘(1st ‘𝑢)) = (2nd ‘(1st ‘𝑡)))
38	37	eqeq1d 2612	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑡 → ((2nd ‘(1st ‘𝑢)) = (𝑝‘1) ↔ (2nd ‘(1st ‘𝑡)) = (𝑝‘1)))
39		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑡 → (2nd ‘𝑢) = (2nd ‘𝑡))
40	39	eqeq1d 2612	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑡 → ((2nd ‘𝑢) = 𝑐 ↔ (2nd ‘𝑡) = 𝑐))
41	36, 38, 40	3anbi123d 1391	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑡 → (((1st ‘(1st ‘𝑢)) = 𝐴 ∧ (2nd ‘(1st ‘𝑢)) = (𝑝‘1) ∧ (2nd ‘𝑢) = 𝑐) ↔ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐)))
42	41	3anbi3d 1397	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑡 → ((𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑢)) = 𝐴 ∧ (2nd ‘(1st ‘𝑢)) = (𝑝‘1) ∧ (2nd ‘𝑢) = 𝑐)) ↔ (𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐))))
43	42	2exbidv 1839	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑡 → (∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑢)) = 𝐴 ∧ (2nd ‘(1st ‘𝑢)) = (𝑝‘1) ∧ (2nd ‘𝑢) = 𝑐)) ↔ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐))))
44	43	elrab 3331	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑢)) = 𝐴 ∧ (2nd ‘(1st ‘𝑢)) = (𝑝‘1) ∧ (2nd ‘𝑢) = 𝑐))} ↔ (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑐))))
45	33, 44	sylnibr 318	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ ∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑞‘1) ∧ (2nd ‘𝑡) = 𝑏))) → ¬ 𝑡 ∈ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑢)) = 𝐴 ∧ (2nd ‘(1st ‘𝑢)) = (𝑝‘1) ∧ (2nd ‘𝑢) = 𝑐))})
46	45	ex 449	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) → (∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑞‘1) ∧ (2nd ‘𝑡) = 𝑏)) → ¬ 𝑡 ∈ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑢)) = 𝐴 ∧ (2nd ‘(1st ‘𝑢)) = (𝑝‘1) ∧ (2nd ‘𝑢) = 𝑐))}))
47	46	ralrimiva 2949	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) → ∀𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)(∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑞‘1) ∧ (2nd ‘𝑡) = 𝑏)) → ¬ 𝑡 ∈ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑢)) = 𝐴 ∧ (2nd ‘(1st ‘𝑢)) = (𝑝‘1) ∧ (2nd ‘𝑢) = 𝑐))}))
48		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 𝑡 → (1st ‘𝑠) = (1st ‘𝑡))
49	48	fveq2d 6107	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑡 → (1st ‘(1st ‘𝑠)) = (1st ‘(1st ‘𝑡)))
50	49	eqeq1d 2612	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑡 → ((1st ‘(1st ‘𝑠)) = 𝐴 ↔ (1st ‘(1st ‘𝑡)) = 𝐴))
51	48	fveq2d 6107	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑡 → (2nd ‘(1st ‘𝑠)) = (2nd ‘(1st ‘𝑡)))
52	51	eqeq1d 2612	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑡 → ((2nd ‘(1st ‘𝑠)) = (𝑞‘1) ↔ (2nd ‘(1st ‘𝑡)) = (𝑞‘1)))
53		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑡 → (2nd ‘𝑠) = (2nd ‘𝑡))
54	53	eqeq1d 2612	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑡 → ((2nd ‘𝑠) = 𝑏 ↔ (2nd ‘𝑡) = 𝑏))
55	50, 52, 54	3anbi123d 1391	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 𝑡 → (((1st ‘(1st ‘𝑠)) = 𝐴 ∧ (2nd ‘(1st ‘𝑠)) = (𝑞‘1) ∧ (2nd ‘𝑠) = 𝑏) ↔ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑞‘1) ∧ (2nd ‘𝑡) = 𝑏)))
56	55	3anbi3d 1397	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑡 → ((𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑠)) = 𝐴 ∧ (2nd ‘(1st ‘𝑠)) = (𝑞‘1) ∧ (2nd ‘𝑠) = 𝑏)) ↔ (𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑞‘1) ∧ (2nd ‘𝑡) = 𝑏))))
57	56	2exbidv 1839	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = 𝑡 → (∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑠)) = 𝐴 ∧ (2nd ‘(1st ‘𝑠)) = (𝑞‘1) ∧ (2nd ‘𝑠) = 𝑏)) ↔ ∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑞‘1) ∧ (2nd ‘𝑡) = 𝑏))))
58	57	ralrab 3335	. . . . . . . . . . . . . 14 ⊢ (∀𝑡 ∈ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑠)) = 𝐴 ∧ (2nd ‘(1st ‘𝑠)) = (𝑞‘1) ∧ (2nd ‘𝑠) = 𝑏))} ¬ 𝑡 ∈ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑢)) = 𝐴 ∧ (2nd ‘(1st ‘𝑢)) = (𝑝‘1) ∧ (2nd ‘𝑢) = 𝑐))} ↔ ∀𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)(∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑞‘1) ∧ (2nd ‘𝑡) = 𝑏)) → ¬ 𝑡 ∈ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑢)) = 𝐴 ∧ (2nd ‘(1st ‘𝑢)) = (𝑝‘1) ∧ (2nd ‘𝑢) = 𝑐))}))
59	47, 58	sylibr 223	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) → ∀𝑡 ∈ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑠)) = 𝐴 ∧ (2nd ‘(1st ‘𝑠)) = (𝑞‘1) ∧ (2nd ‘𝑠) = 𝑏))} ¬ 𝑡 ∈ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑢)) = 𝐴 ∧ (2nd ‘(1st ‘𝑢)) = (𝑝‘1) ∧ (2nd ‘𝑢) = 𝑐))})
60		disj 3969	. . . . . . . . . . . . 13 ⊢ (({𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑠)) = 𝐴 ∧ (2nd ‘(1st ‘𝑠)) = (𝑞‘1) ∧ (2nd ‘𝑠) = 𝑏))} ∩ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑢)) = 𝐴 ∧ (2nd ‘(1st ‘𝑢)) = (𝑝‘1) ∧ (2nd ‘𝑢) = 𝑐))}) = ∅ ↔ ∀𝑡 ∈ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑠)) = 𝐴 ∧ (2nd ‘(1st ‘𝑠)) = (𝑞‘1) ∧ (2nd ‘𝑠) = 𝑏))} ¬ 𝑡 ∈ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑢)) = 𝐴 ∧ (2nd ‘(1st ‘𝑢)) = (𝑝‘1) ∧ (2nd ‘𝑢) = 𝑐))})
61	59, 60	sylibr 223	. . . . . . . . . . . 12 ⊢ ((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) → ({𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑔∃𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st ‘𝑠)) = 𝐴 ∧ (2nd ‘(1st ‘𝑠)) = (𝑞‘1) ∧ (2nd ‘𝑠) = 𝑏))} ∩ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑢)) = 𝐴 ∧ (2nd ‘(1st ‘𝑢)) = (𝑝‘1) ∧ (2nd ‘𝑢) = 𝑐))}) = ∅)
62	11, 61	eqtrd 2644	. . . . . . . . . . 11 ⊢ ((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) → ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅)
63	62	olcd 407	. . . . . . . . . 10 ⊢ ((¬ 𝑏 = 𝑐 ∧ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴})) → (𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅))
64	63	ex 449	. . . . . . . . 9 ⊢ (¬ 𝑏 = 𝑐 → (((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴}) → (𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅)))
65	2, 64	pm2.61i 175	. . . . . . . 8 ⊢ (((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) ∧ 𝑐 ∉ {𝐴}) → (𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅))
66	65	ex 449	. . . . . . 7 ⊢ ((((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐 ∈ 𝑉) → (𝑐 ∉ {𝐴} → (𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅)))
67	66	ralrimiva 2949	. . . . . 6 ⊢ (((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) → ∀𝑐 ∈ 𝑉 (𝑐 ∉ {𝐴} → (𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅)))
68		raldifb 3712	. . . . . 6 ⊢ (∀𝑐 ∈ 𝑉 (𝑐 ∉ {𝐴} → (𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅)) ↔ ∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅))
69	67, 68	sylib 207	. . . . 5 ⊢ (((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) ∧ 𝑏 ∉ {𝐴}) → ∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅))
70	69	ex 449	. . . 4 ⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) → (𝑏 ∉ {𝐴} → ∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅)))
71	70	ralrimiva 2949	. . 3 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) → ∀𝑏 ∈ 𝑉 (𝑏 ∉ {𝐴} → ∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅)))
72		raldifb 3712	. . 3 ⊢ (∀𝑏 ∈ 𝑉 (𝑏 ∉ {𝐴} → ∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅)) ↔ ∀𝑏 ∈ (𝑉 ∖ {𝐴})∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅))
73	71, 72	sylib 207	. 2 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) → ∀𝑏 ∈ (𝑉 ∖ {𝐴})∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅))
74		oveq2 6557	. . 3 ⊢ (𝑏 = 𝑐 → (𝐴(𝑉 2SPathOnOt 𝐸)𝑏) = (𝐴(𝑉 2SPathOnOt 𝐸)𝑐))
75	74	disjor 4567	. 2 ⊢ (Disj 𝑏 ∈ (𝑉 ∖ {𝐴})(𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ↔ ∀𝑏 ∈ (𝑉 ∖ {𝐴})∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅))
76	73, 75	sylibr 223	1 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) → Disj 𝑏 ∈ (𝑉 ∖ {𝐴})(𝐴(𝑉 2SPathOnOt 𝐸)𝑏))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382   ∧ wa 383   ∨ w3o 1030   ∧ w3a 1031  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ∉ wnel 2781  ∀wral 2896  {crab 2900   ∖ cdif 3537   ∩ cin 3539  ∅c0 3874  {csn 4125  Disj wdisj 4553   class class class wbr 4583   × cxp 5036  ‘cfv 5804  (class class class)co 6549  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-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-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-disj 4554  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:  frghash2spot  26590