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

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.
StepHypRef Expression
1 orc 399 . . . . . . . . . 10 (𝑏 = 𝑐 → (𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅))
21a1d 25 . . . . . . . . 9 (𝑏 = 𝑐 → (((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴}) → (𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅)))
3 2spthonot 26393 . . . . . . . . . . . . . . . . 17 (((𝑉𝑋𝐸𝑌) ∧ (𝐴𝑉𝑏𝑉)) → (𝐴(𝑉 2SPathOnOt 𝐸)𝑏) = {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑔𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑠)) = 𝐴 ∧ (2nd ‘(1st𝑠)) = (𝑞‘1) ∧ (2nd𝑠) = 𝑏))})
43anassrs 678 . . . . . . . . . . . . . . . 16 ((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) → (𝐴(𝑉 2SPathOnOt 𝐸)𝑏) = {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑔𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑠)) = 𝐴 ∧ (2nd ‘(1st𝑠)) = (𝑞‘1) ∧ (2nd𝑠) = 𝑏))})
54adantr 480 . . . . . . . . . . . . . . 15 (((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑐𝑉) → (𝐴(𝑉 2SPathOnOt 𝐸)𝑏) = {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑔𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑠)) = 𝐴 ∧ (2nd ‘(1st𝑠)) = (𝑞‘1) ∧ (2nd𝑠) = 𝑏))})
6 2spthonot 26393 . . . . . . . . . . . . . . . . 17 (((𝑉𝑋𝐸𝑌) ∧ (𝐴𝑉𝑐𝑉)) → (𝐴(𝑉 2SPathOnOt 𝐸)𝑐) = {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑢)) = 𝐴 ∧ (2nd ‘(1st𝑢)) = (𝑝‘1) ∧ (2nd𝑢) = 𝑐))})
76anassrs 678 . . . . . . . . . . . . . . . 16 ((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑐𝑉) → (𝐴(𝑉 2SPathOnOt 𝐸)𝑐) = {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑢)) = 𝐴 ∧ (2nd ‘(1st𝑢)) = (𝑝‘1) ∧ (2nd𝑢) = 𝑐))})
87adantlr 747 . . . . . . . . . . . . . . 15 (((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑐𝑉) → (𝐴(𝑉 2SPathOnOt 𝐸)𝑐) = {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑢)) = 𝐴 ∧ (2nd ‘(1st𝑢)) = (𝑝‘1) ∧ (2nd𝑢) = 𝑐))})
95, 8ineq12d 3777 . . . . . . . . . . . . . 14 (((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑐𝑉) → ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ({𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑔𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑠)) = 𝐴 ∧ (2nd ‘(1st𝑠)) = (𝑞‘1) ∧ (2nd𝑠) = 𝑏))} ∩ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑢)) = 𝐴 ∧ (2nd ‘(1st𝑢)) = (𝑝‘1) ∧ (2nd𝑢) = 𝑐))}))
109adantlr 747 . . . . . . . . . . . . 13 ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) → ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ({𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑔𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑠)) = 𝐴 ∧ (2nd ‘(1st𝑠)) = (𝑞‘1) ∧ (2nd𝑠) = 𝑏))} ∩ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑢)) = 𝐴 ∧ (2nd ‘(1st𝑢)) = (𝑝‘1) ∧ (2nd𝑢) = 𝑐))}))
1110ad2antrl 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𝑡) = 𝑐) → 𝑏 = 𝑐)
1312ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((2nd𝑡) = 𝑏 → ((2nd𝑡) = 𝑐𝑏 = 𝑐))
1413con3rr3 150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑏 = 𝑐 → ((2nd𝑡) = 𝑏 → ¬ (2nd𝑡) = 𝑐))
1514adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((¬ 𝑏 = 𝑐 ∧ ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴})) → ((2nd𝑡) = 𝑏 → ¬ (2nd𝑡) = 𝑐))
1615adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((¬ 𝑏 = 𝑐 ∧ ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) → ((2nd𝑡) = 𝑏 → ¬ (2nd𝑡) = 𝑐))
1716com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑡) = 𝑏 → (((¬ 𝑏 = 𝑐 ∧ ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) → ¬ (2nd𝑡) = 𝑐))
18173ad2ant3 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑞‘1) ∧ (2nd𝑡) = 𝑏) → (((¬ 𝑏 = 𝑐 ∧ ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) → ¬ (2nd𝑡) = 𝑐))
19183ad2ant3 1077 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑞‘1) ∧ (2nd𝑡) = 𝑏)) → (((¬ 𝑏 = 𝑐 ∧ ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) → ¬ (2nd𝑡) = 𝑐))
2019impcom 445 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((¬ 𝑏 = 𝑐 ∧ ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ (𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑞‘1) ∧ (2nd𝑡) = 𝑏))) → ¬ (2nd𝑡) = 𝑐)
2120intn3an3d 1436 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((¬ 𝑏 = 𝑐 ∧ ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ (𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑞‘1) ∧ (2nd𝑡) = 𝑏))) → ¬ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑐))
22213mix3d 1231 . . . . . . . . . . . . . . . . . . . . . . 23 ((((¬ 𝑏 = 𝑐 ∧ ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ (𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑞‘1) ∧ (2nd𝑡) = 𝑏))) → (¬ 𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∨ ¬ (#‘𝑓) = 2 ∨ ¬ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑐)))
2322ex 449 . . . . . . . . . . . . . . . . . . . . . 22 (((¬ 𝑏 = 𝑐 ∧ ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) → ((𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑞‘1) ∧ (2nd𝑡) = 𝑏)) → (¬ 𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∨ ¬ (#‘𝑓) = 2 ∨ ¬ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑐))))
2423exlimdvv 1849 . . . . . . . . . . . . . . . . . . . . 21 (((¬ 𝑏 = 𝑐 ∧ ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) → (∃𝑔𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑞‘1) ∧ (2nd𝑡) = 𝑏)) → (¬ 𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∨ ¬ (#‘𝑓) = 2 ∨ ¬ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑐))))
2524imp 444 . . . . . . . . . . . . . . . . . . . 20 ((((¬ 𝑏 = 𝑐 ∧ ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ ∃𝑔𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑞‘1) ∧ (2nd𝑡) = 𝑏))) → (¬ 𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∨ ¬ (#‘𝑓) = 2 ∨ ¬ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑐)))
2625alrimivv 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𝑡) = 𝑐)))
2928bicomi 213 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∨ ¬ (#‘𝑓) = 2 ∨ ¬ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑐)) ↔ ¬ (𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑐)))
30292albii 1738 . . . . . . . . . . . . . . . . . . . 20 (∀𝑓𝑝𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∨ ¬ (#‘𝑓) = 2 ∨ ¬ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑐)) ↔ ∀𝑓𝑝 ¬ (𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑐)))
3127, 30bitr4i 266 . . . . . . . . . . . . . . . . . . 19 (¬ ∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑐)) ↔ ∀𝑓𝑝𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∨ ¬ (#‘𝑓) = 2 ∨ ¬ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑐)))
3226, 31sylibr 223 . . . . . . . . . . . . . . . . . 18 ((((¬ 𝑏 = 𝑐 ∧ ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ ∃𝑔𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑞‘1) ∧ (2nd𝑡) = 𝑏))) → ¬ ∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑐)))
3332intnand 953 . . . . . . . . . . . . . . . . 17 ((((¬ 𝑏 = 𝑐 ∧ ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ ∃𝑔𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑞‘1) ∧ (2nd𝑡) = 𝑏))) → ¬ (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑐))))
34 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑡 → (1st𝑢) = (1st𝑡))
3534fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑡 → (1st ‘(1st𝑢)) = (1st ‘(1st𝑡)))
3635eqeq1d 2612 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑡 → ((1st ‘(1st𝑢)) = 𝐴 ↔ (1st ‘(1st𝑡)) = 𝐴))
3734fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑡 → (2nd ‘(1st𝑢)) = (2nd ‘(1st𝑡)))
3837eqeq1d 2612 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑡 → ((2nd ‘(1st𝑢)) = (𝑝‘1) ↔ (2nd ‘(1st𝑡)) = (𝑝‘1)))
39 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑡 → (2nd𝑢) = (2nd𝑡))
4039eqeq1d 2612 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑡 → ((2nd𝑢) = 𝑐 ↔ (2nd𝑡) = 𝑐))
4136, 38, 403anbi123d 1391 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑡 → (((1st ‘(1st𝑢)) = 𝐴 ∧ (2nd ‘(1st𝑢)) = (𝑝‘1) ∧ (2nd𝑢) = 𝑐) ↔ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑐)))
42413anbi3d 1397 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑡 → ((𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑢)) = 𝐴 ∧ (2nd ‘(1st𝑢)) = (𝑝‘1) ∧ (2nd𝑢) = 𝑐)) ↔ (𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑐))))
43422exbidv 1839 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑡 → (∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑢)) = 𝐴 ∧ (2nd ‘(1st𝑢)) = (𝑝‘1) ∧ (2nd𝑢) = 𝑐)) ↔ ∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑐))))
4443elrab 3331 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑢)) = 𝐴 ∧ (2nd ‘(1st𝑢)) = (𝑝‘1) ∧ (2nd𝑢) = 𝑐))} ↔ (𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑐))))
4533, 44sylnibr 318 . . . . . . . . . . . . . . . 16 ((((¬ 𝑏 = 𝑐 ∧ ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ ∃𝑔𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑞‘1) ∧ (2nd𝑡) = 𝑏))) → ¬ 𝑡 ∈ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑢)) = 𝐴 ∧ (2nd ‘(1st𝑢)) = (𝑝‘1) ∧ (2nd𝑢) = 𝑐))})
4645ex 449 . . . . . . . . . . . . . . 15 (((¬ 𝑏 = 𝑐 ∧ ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴})) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) → (∃𝑔𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑞‘1) ∧ (2nd𝑡) = 𝑏)) → ¬ 𝑡 ∈ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑢)) = 𝐴 ∧ (2nd ‘(1st𝑢)) = (𝑝‘1) ∧ (2nd𝑢) = 𝑐))}))
4746ralrimiva 2949 . . . . . . . . . . . . . 14 ((¬ 𝑏 = 𝑐 ∧ ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴})) → ∀𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)(∃𝑔𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑞‘1) ∧ (2nd𝑡) = 𝑏)) → ¬ 𝑡 ∈ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑢)) = 𝐴 ∧ (2nd ‘(1st𝑢)) = (𝑝‘1) ∧ (2nd𝑢) = 𝑐))}))
48 fveq2 6103 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑡 → (1st𝑠) = (1st𝑡))
4948fveq2d 6107 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → (1st ‘(1st𝑠)) = (1st ‘(1st𝑡)))
5049eqeq1d 2612 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑡 → ((1st ‘(1st𝑠)) = 𝐴 ↔ (1st ‘(1st𝑡)) = 𝐴))
5148fveq2d 6107 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → (2nd ‘(1st𝑠)) = (2nd ‘(1st𝑡)))
5251eqeq1d 2612 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑡 → ((2nd ‘(1st𝑠)) = (𝑞‘1) ↔ (2nd ‘(1st𝑡)) = (𝑞‘1)))
53 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → (2nd𝑠) = (2nd𝑡))
5453eqeq1d 2612 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑡 → ((2nd𝑠) = 𝑏 ↔ (2nd𝑡) = 𝑏))
5550, 52, 543anbi123d 1391 . . . . . . . . . . . . . . . . 17 (𝑠 = 𝑡 → (((1st ‘(1st𝑠)) = 𝐴 ∧ (2nd ‘(1st𝑠)) = (𝑞‘1) ∧ (2nd𝑠) = 𝑏) ↔ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑞‘1) ∧ (2nd𝑡) = 𝑏)))
56553anbi3d 1397 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑡 → ((𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑠)) = 𝐴 ∧ (2nd ‘(1st𝑠)) = (𝑞‘1) ∧ (2nd𝑠) = 𝑏)) ↔ (𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑞‘1) ∧ (2nd𝑡) = 𝑏))))
57562exbidv 1839 . . . . . . . . . . . . . . 15 (𝑠 = 𝑡 → (∃𝑔𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑠)) = 𝐴 ∧ (2nd ‘(1st𝑠)) = (𝑞‘1) ∧ (2nd𝑠) = 𝑏)) ↔ ∃𝑔𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑞‘1) ∧ (2nd𝑡) = 𝑏))))
5857ralrab 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𝑢) = 𝑐))}))
5947, 58sylibr 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𝑢) = 𝑐))})
6159, 60sylibr 223 . . . . . . . . . . . 12 ((¬ 𝑏 = 𝑐 ∧ ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴})) → ({𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑔𝑞(𝑔(𝐴(𝑉 SPathOn 𝐸)𝑏)𝑞 ∧ (#‘𝑔) = 2 ∧ ((1st ‘(1st𝑠)) = 𝐴 ∧ (2nd ‘(1st𝑠)) = (𝑞‘1) ∧ (2nd𝑠) = 𝑏))} ∩ {𝑢 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝑐)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑢)) = 𝐴 ∧ (2nd ‘(1st𝑢)) = (𝑝‘1) ∧ (2nd𝑢) = 𝑐))}) = ∅)
6211, 61eqtrd 2644 . . . . . . . . . . 11 ((¬ 𝑏 = 𝑐 ∧ ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴})) → ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅)
6362olcd 407 . . . . . . . . . 10 ((¬ 𝑏 = 𝑐 ∧ ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴})) → (𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅))
6463ex 449 . . . . . . . . 9 𝑏 = 𝑐 → (((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴}) → (𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅)))
652, 64pm2.61i 175 . . . . . . . 8 (((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) ∧ 𝑐 ∉ {𝐴}) → (𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅))
6665ex 449 . . . . . . 7 ((((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) ∧ 𝑐𝑉) → (𝑐 ∉ {𝐴} → (𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅)))
6766ralrimiva 2949 . . . . . 6 (((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) → ∀𝑐𝑉 (𝑐 ∉ {𝐴} → (𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅)))
68 raldifb 3712 . . . . . 6 (∀𝑐𝑉 (𝑐 ∉ {𝐴} → (𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅)) ↔ ∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅))
6967, 68sylib 207 . . . . 5 (((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) ∧ 𝑏 ∉ {𝐴}) → ∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅))
7069ex 449 . . . 4 ((((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) ∧ 𝑏𝑉) → (𝑏 ∉ {𝐴} → ∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅)))
7170ralrimiva 2949 . . 3 (((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) → ∀𝑏𝑉 (𝑏 ∉ {𝐴} → ∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅)))
72 raldifb 3712 . . 3 (∀𝑏𝑉 (𝑏 ∉ {𝐴} → ∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅)) ↔ ∀𝑏 ∈ (𝑉 ∖ {𝐴})∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅))
7371, 72sylib 207 . 2 (((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) → ∀𝑏 ∈ (𝑉 ∖ {𝐴})∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅))
74 oveq2 6557 . . 3 (𝑏 = 𝑐 → (𝐴(𝑉 2SPathOnOt 𝐸)𝑏) = (𝐴(𝑉 2SPathOnOt 𝐸)𝑐))
7574disjor 4567 . 2 (Disj 𝑏 ∈ (𝑉 ∖ {𝐴})(𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ↔ ∀𝑏 ∈ (𝑉 ∖ {𝐴})∀𝑐 ∈ (𝑉 ∖ {𝐴})(𝑏 = 𝑐 ∨ ((𝐴(𝑉 2SPathOnOt 𝐸)𝑏) ∩ (𝐴(𝑉 2SPathOnOt 𝐸)𝑐)) = ∅))
7673, 75sylibr 223 1 (((𝑉𝑋𝐸𝑌) ∧ 𝐴𝑉) → Disj 𝑏 ∈ (𝑉 ∖ {𝐴})(𝐴(𝑉 2SPathOnOt 𝐸)𝑏))
 Colors of variables: wff setvar class 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  1st c1st 7057  2nd 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
 Copyright terms: Public domain W3C validator