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.
StepHypRef Expression
1 ne0i 3880 . . 3 (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) ≠ ∅)
2 df-ov 6552 . . . . 5 (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) = ((𝑉 2SPathOnOt 𝐸)‘⟨𝐴, 𝐶⟩)
3 ndmfv 6128 . . . . 5 (¬ ⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → ((𝑉 2SPathOnOt 𝐸)‘⟨𝐴, 𝐶⟩) = ∅)
42, 3syl5eq 2656 . . . 4 (¬ ⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) = ∅)
54necon1ai 2809 . . 3 ((𝐴(𝑉 2SPathOnOt 𝐸)𝐶) ≠ ∅ → ⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸))
6 simpl 472 . . . . . . . . 9 ((𝑣 = 𝑉𝑒 = 𝐸) → 𝑣 = 𝑉)
7 id 22 . . . . . . . . . . . . 13 (𝑣 = 𝑉𝑣 = 𝑉)
87, 7xpeq12d 5064 . . . . . . . . . . . 12 (𝑣 = 𝑉 → (𝑣 × 𝑣) = (𝑉 × 𝑉))
98, 7xpeq12d 5064 . . . . . . . . . . 11 (𝑣 = 𝑉 → ((𝑣 × 𝑣) × 𝑣) = ((𝑉 × 𝑉) × 𝑉))
109adantr 480 . . . . . . . . . 10 ((𝑣 = 𝑉𝑒 = 𝐸) → ((𝑣 × 𝑣) × 𝑣) = ((𝑉 × 𝑉) × 𝑉))
11 oveq12 6558 . . . . . . . . . . . . . 14 ((𝑣 = 𝑉𝑒 = 𝐸) → (𝑣 SPathOn 𝑒) = (𝑉 SPathOn 𝐸))
1211oveqd 6566 . . . . . . . . . . . . 13 ((𝑣 = 𝑉𝑒 = 𝐸) → (𝑎(𝑣 SPathOn 𝑒)𝑏) = (𝑎(𝑉 SPathOn 𝐸)𝑏))
1312breqd 4594 . . . . . . . . . . . 12 ((𝑣 = 𝑉𝑒 = 𝐸) → (𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝))
14133anbi1d 1395 . . . . . . . . . . 11 ((𝑣 = 𝑉𝑒 = 𝐸) → ((𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏)) ↔ (𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))))
15142exbidv 1839 . . . . . . . . . 10 ((𝑣 = 𝑉𝑒 = 𝐸) → (∃𝑓𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏)) ↔ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))))
1610, 15rabeqbidv 3168 . . . . . . . . 9 ((𝑣 = 𝑉𝑒 = 𝐸) → {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))} = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))})
176, 6, 16mpt2eq123dv 6615 . . . . . . . 8 ((𝑣 = 𝑉𝑒 = 𝐸) → (𝑎𝑣, 𝑏𝑣 ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) = (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}))
18 df-2spthonot 26387 . . . . . . . 8 2SPathOnOt = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎𝑣, 𝑏𝑣 ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}))
1917, 18ovmpt2ga 6688 . . . . . . 7 ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V) → (𝑉 2SPathOnOt 𝐸) = (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}))
2019dmeqd 5248 . . . . . 6 ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V) → dom (𝑉 2SPathOnOt 𝐸) = dom (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}))
2120eleq2d 2673 . . . . 5 ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) ↔ ⟨𝐴, 𝐶⟩ ∈ dom (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))})))
22 dmoprabss 6640 . . . . . . . . 9 dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎𝑉𝑏𝑉) ∧ 𝑐 = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))})} ⊆ (𝑉 × 𝑉)
2322sseli 3564 . . . . . . . 8 (⟨𝐴, 𝐶⟩ ∈ dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎𝑉𝑏𝑉) ∧ 𝑐 = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))})} → ⟨𝐴, 𝐶⟩ ∈ (𝑉 × 𝑉))
24 opelxp 5070 . . . . . . . . . . . 12 (⟨𝐴, 𝐶⟩ ∈ (𝑉 × 𝑉) ↔ (𝐴𝑉𝐶𝑉))
25 2spthonot 26393 . . . . . . . . . . . . . . 15 (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉)) → (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝐶))})
2625eleq2d 2673 . . . . . . . . . . . . . 14 (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉)) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) ↔ 𝑇 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝐶))}))
27 elrabi 3328 . . . . . . . . . . . . . . 15 (𝑇 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝐶))} → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))
28 simpl 472 . . . . . . . . . . . . . . . . . 18 (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉)) → (𝑉 ∈ V ∧ 𝐸 ∈ V))
2928adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉)) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)) → (𝑉 ∈ V ∧ 𝐸 ∈ V))
30 simpr 476 . . . . . . . . . . . . . . . . . 18 (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉)) → (𝐴𝑉𝐶𝑉))
3130adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉)) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)) → (𝐴𝑉𝐶𝑉))
32 simpr 476 . . . . . . . . . . . . . . . . 17 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉)) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))
3329, 31, 323jca 1235 . . . . . . . . . . . . . . . 16 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉)) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))
3433ex 449 . . . . . . . . . . . . . . 15 (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉)) → (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))))
3527, 34syl5 33 . . . . . . . . . . . . . 14 (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉)) → (𝑇 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝐴 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝐶))} → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))))
3626, 35sylbid 229 . . . . . . . . . . . . 13 (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉)) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))))
3736expcom 450 . . . . . . . . . . . 12 ((𝐴𝑉𝐶𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
3824, 37sylbi 206 . . . . . . . . . . 11 (⟨𝐴, 𝐶⟩ ∈ (𝑉 × 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
3938com12 32 . . . . . . . . . 10 ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (⟨𝐴, 𝐶⟩ ∈ (𝑉 × 𝑉) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
40393adant3 1074 . . . . . . . . 9 ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V) → (⟨𝐴, 𝐶⟩ ∈ (𝑉 × 𝑉) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
4140com12 32 . . . . . . . 8 (⟨𝐴, 𝐶⟩ ∈ (𝑉 × 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
4223, 41syl 17 . . . . . . 7 (⟨𝐴, 𝐶⟩ ∈ dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎𝑉𝑏𝑉) ∧ 𝑐 = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))})} → ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
43 df-mpt2 6554 . . . . . . . 8 (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) = {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎𝑉𝑏𝑉) ∧ 𝑐 = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))})}
4443dmeqi 5247 . . . . . . 7 dom (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) = dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎𝑉𝑏𝑉) ∧ 𝑐 = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))})}
4542, 44eleq2s 2706 . . . . . 6 (⟨𝐴, 𝐶⟩ ∈ dom (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) → ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
4645com12 32 . . . . 5 ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
4721, 46sylbid 229 . . . 4 ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
48 3ianor 1048 . . . . 5 (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V) ↔ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V))
49 df-3or 1032 . . . . . 6 ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V) ↔ ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) ∨ ¬ (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V))
50 ianor 508 . . . . . . . 8 (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) ↔ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V))
5118mpt2ndm0 6773 . . . . . . . . . . . 12 (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 2SPathOnOt 𝐸) = ∅)
5251dmeqd 5248 . . . . . . . . . . 11 (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → dom (𝑉 2SPathOnOt 𝐸) = dom ∅)
5352eleq2d 2673 . . . . . . . . . 10 (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) ↔ ⟨𝐴, 𝐶⟩ ∈ dom ∅))
54 dm0 5260 . . . . . . . . . . 11 dom ∅ = ∅
5554eleq2i 2680 . . . . . . . . . 10 (⟨𝐴, 𝐶⟩ ∈ dom ∅ ↔ ⟨𝐴, 𝐶⟩ ∈ ∅)
5653, 55syl6bb 275 . . . . . . . . 9 (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) ↔ ⟨𝐴, 𝐶⟩ ∈ ∅))
57 noel 3878 . . . . . . . . . 10 ¬ ⟨𝐴, 𝐶⟩ ∈ ∅
5857pm2.21i 115 . . . . . . . . 9 (⟨𝐴, 𝐶⟩ ∈ ∅ → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))))
5956, 58syl6bi 242 . . . . . . . 8 (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
6050, 59sylbir 224 . . . . . . 7 ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
61 anor 509 . . . . . . . . 9 ((𝑉 ∈ V ∧ 𝐸 ∈ V) ↔ ¬ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V))
62 id 22 . . . . . . . . . . . . 13 (𝑉 ∈ V → 𝑉 ∈ V)
6362ancri 573 . . . . . . . . . . . 12 (𝑉 ∈ V → (𝑉 ∈ V ∧ 𝑉 ∈ V))
6463adantr 480 . . . . . . . . . . 11 ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ∈ V ∧ 𝑉 ∈ V))
65 mpt2exga 7135 . . . . . . . . . . 11 ((𝑉 ∈ V ∧ 𝑉 ∈ V) → (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V)
6664, 65syl 17 . . . . . . . . . 10 ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V)
6766pm2.24d 146 . . . . . . . . 9 ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (¬ (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))))))
6861, 67sylbir 224 . . . . . . . 8 (¬ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) → (¬ (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))))))
6968imp 444 . . . . . . 7 ((¬ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) ∧ ¬ (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
7060, 69jaoi3 1003 . . . . . 6 (((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) ∨ ¬ (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
7149, 70sylbi 206 . . . . 5 ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
7248, 71sylbi 206 . . . 4 (¬ (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎𝑉, 𝑏𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}) ∈ V) → (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))))
7347, 72pm2.61i 175 . . 3 (⟨𝐴, 𝐶⟩ ∈ dom (𝑉 2SPathOnOt 𝐸) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))))
741, 5, 733syl 18 . 2 (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴𝑉𝐶𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))))
7574pm2.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  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-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
 Copyright terms: Public domain W3C validator