Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  uhgr2edg Structured version   Visualization version   GIF version

Theorem uhgr2edg 40435
 Description: If a vertex is adjacent to two different vertices in a hypergraph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 11-Feb-2021.)
Hypotheses
Ref Expression
usgrf1oedg.i 𝐼 = (iEdg‘𝐺)
usgrf1oedg.e 𝐸 = (Edg‘𝐺)
uhgr2edg.v 𝑉 = (Vtx‘𝐺)
Assertion
Ref Expression
uhgr2edg (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦)))
Distinct variable groups:   𝑥,𝐺   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑦,𝐺   𝑥,𝐼,𝑦   𝑥,𝑁,𝑦   𝑥,𝑉,𝑦
Allowed substitution hints:   𝐸(𝑥,𝑦)

Proof of Theorem uhgr2edg
StepHypRef Expression
1 simp1l 1078 . . . 4 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐺 ∈ UHGraph )
2 simp1r 1079 . . . 4 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐴𝐵)
3 simp23 1089 . . . . 5 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝑁𝑉)
4 simp21 1087 . . . . 5 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐴𝑉)
5 3simpc 1053 . . . . . 6 ((𝐴𝑉𝐵𝑉𝑁𝑉) → (𝐵𝑉𝑁𝑉))
653ad2ant2 1076 . . . . 5 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → (𝐵𝑉𝑁𝑉))
73, 4, 6jca31 555 . . . 4 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)))
81, 2, 7jca31 555 . . 3 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))))
9 simp3 1056 . . 3 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸))
108, 9jca 553 . 2 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)))
11 usgrf1oedg.e . . . . . . . . . 10 𝐸 = (Edg‘𝐺)
1211a1i 11 . . . . . . . . 9 (𝐺 ∈ UHGraph → 𝐸 = (Edg‘𝐺))
13 edgaval 25794 . . . . . . . . 9 (𝐺 ∈ UHGraph → (Edg‘𝐺) = ran (iEdg‘𝐺))
14 usgrf1oedg.i . . . . . . . . . . . 12 𝐼 = (iEdg‘𝐺)
1514eqcomi 2619 . . . . . . . . . . 11 (iEdg‘𝐺) = 𝐼
1615a1i 11 . . . . . . . . . 10 (𝐺 ∈ UHGraph → (iEdg‘𝐺) = 𝐼)
1716rneqd 5274 . . . . . . . . 9 (𝐺 ∈ UHGraph → ran (iEdg‘𝐺) = ran 𝐼)
1812, 13, 173eqtrd 2648 . . . . . . . 8 (𝐺 ∈ UHGraph → 𝐸 = ran 𝐼)
1918eleq2d 2673 . . . . . . 7 (𝐺 ∈ UHGraph → ({𝑁, 𝐴} ∈ 𝐸 ↔ {𝑁, 𝐴} ∈ ran 𝐼))
2018eleq2d 2673 . . . . . . 7 (𝐺 ∈ UHGraph → ({𝐵, 𝑁} ∈ 𝐸 ↔ {𝐵, 𝑁} ∈ ran 𝐼))
2119, 20anbi12d 743 . . . . . 6 (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ ({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼)))
22 eqid 2610 . . . . . . . . . 10 (iEdg‘𝐺) = (iEdg‘𝐺)
2322uhgrfun 25732 . . . . . . . . 9 (𝐺 ∈ UHGraph → Fun (iEdg‘𝐺))
2414funeqi 5824 . . . . . . . . 9 (Fun 𝐼 ↔ Fun (iEdg‘𝐺))
2523, 24sylibr 223 . . . . . . . 8 (𝐺 ∈ UHGraph → Fun 𝐼)
26 funfn 5833 . . . . . . . 8 (Fun 𝐼𝐼 Fn dom 𝐼)
2725, 26sylib 207 . . . . . . 7 (𝐺 ∈ UHGraph → 𝐼 Fn dom 𝐼)
28 fvelrnb 6153 . . . . . . . 8 (𝐼 Fn dom 𝐼 → ({𝑁, 𝐴} ∈ ran 𝐼 ↔ ∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴}))
29 fvelrnb 6153 . . . . . . . 8 (𝐼 Fn dom 𝐼 → ({𝐵, 𝑁} ∈ ran 𝐼 ↔ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁}))
3028, 29anbi12d 743 . . . . . . 7 (𝐼 Fn dom 𝐼 → (({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁})))
3127, 30syl 17 . . . . . 6 (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁})))
3221, 31bitrd 267 . . . . 5 (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁})))
3332ad2antrr 758 . . . 4 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁})))
34 reeanv 3086 . . . . 5 (∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁}))
35 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝐼𝑥) = (𝐼𝑦))
3635eqeq1d 2612 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝐼𝑥) = {𝑁, 𝐴} ↔ (𝐼𝑦) = {𝑁, 𝐴}))
3736anbi1d 737 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) ↔ ((𝐼𝑦) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})))
38 eqtr2 2630 . . . . . . . . . . . . . 14 (((𝐼𝑦) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → {𝑁, 𝐴} = {𝐵, 𝑁})
39 prcom 4211 . . . . . . . . . . . . . . . 16 {𝐵, 𝑁} = {𝑁, 𝐵}
4039eqeq2i 2622 . . . . . . . . . . . . . . 15 ({𝑁, 𝐴} = {𝐵, 𝑁} ↔ {𝑁, 𝐴} = {𝑁, 𝐵})
41 preq12bg 4326 . . . . . . . . . . . . . . . . . . 19 (((𝑁𝑉𝐴𝑉) ∧ (𝑁𝑉𝐵𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} ↔ ((𝑁 = 𝑁𝐴 = 𝐵) ∨ (𝑁 = 𝐵𝐴 = 𝑁))))
4241ancom2s 840 . . . . . . . . . . . . . . . . . 18 (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} ↔ ((𝑁 = 𝑁𝐴 = 𝐵) ∨ (𝑁 = 𝐵𝐴 = 𝑁))))
43 eqneqall 2793 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 = 𝐵 → (𝐴𝐵𝑥𝑦))
4443adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 = 𝑁𝐴 = 𝐵) → (𝐴𝐵𝑥𝑦))
45 eqtr 2629 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 = 𝑁𝑁 = 𝐵) → 𝐴 = 𝐵)
4645ancoms 468 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 = 𝐵𝐴 = 𝑁) → 𝐴 = 𝐵)
4746, 43syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 = 𝐵𝐴 = 𝑁) → (𝐴𝐵𝑥𝑦))
4844, 47jaoi 393 . . . . . . . . . . . . . . . . . . 19 (((𝑁 = 𝑁𝐴 = 𝐵) ∨ (𝑁 = 𝐵𝐴 = 𝑁)) → (𝐴𝐵𝑥𝑦))
4948adantld 482 . . . . . . . . . . . . . . . . . 18 (((𝑁 = 𝑁𝐴 = 𝐵) ∨ (𝑁 = 𝐵𝐴 = 𝑁)) → ((𝐺 ∈ UHGraph ∧ 𝐴𝐵) → 𝑥𝑦))
5042, 49syl6bi 242 . . . . . . . . . . . . . . . . 17 (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} → ((𝐺 ∈ UHGraph ∧ 𝐴𝐵) → 𝑥𝑦)))
5150com3l 87 . . . . . . . . . . . . . . . 16 ({𝑁, 𝐴} = {𝑁, 𝐵} → ((𝐺 ∈ UHGraph ∧ 𝐴𝐵) → (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → 𝑥𝑦)))
5251impd 446 . . . . . . . . . . . . . . 15 ({𝑁, 𝐴} = {𝑁, 𝐵} → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑥𝑦))
5340, 52sylbi 206 . . . . . . . . . . . . . 14 ({𝑁, 𝐴} = {𝐵, 𝑁} → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑥𝑦))
5438, 53syl 17 . . . . . . . . . . . . 13 (((𝐼𝑦) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑥𝑦))
5537, 54syl6bi 242 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑥𝑦)))
5655com23 84 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → 𝑥𝑦)))
5756impd 446 . . . . . . . . . 10 (𝑥 = 𝑦 → ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑥𝑦))
58 ax-1 6 . . . . . . . . . 10 (𝑥𝑦 → ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑥𝑦))
5957, 58pm2.61ine 2865 . . . . . . . . 9 ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑥𝑦)
60 prid1g 4239 . . . . . . . . . . . . . 14 (𝑁𝑉𝑁 ∈ {𝑁, 𝐴})
6160ad2antrr 758 . . . . . . . . . . . . 13 (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → 𝑁 ∈ {𝑁, 𝐴})
6261adantl 481 . . . . . . . . . . . 12 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ {𝑁, 𝐴})
63 eleq2 2677 . . . . . . . . . . . 12 ((𝐼𝑥) = {𝑁, 𝐴} → (𝑁 ∈ (𝐼𝑥) ↔ 𝑁 ∈ {𝑁, 𝐴}))
6462, 63syl5ibr 235 . . . . . . . . . . 11 ((𝐼𝑥) = {𝑁, 𝐴} → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ (𝐼𝑥)))
6564adantr 480 . . . . . . . . . 10 (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ (𝐼𝑥)))
6665impcom 445 . . . . . . . . 9 ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑁 ∈ (𝐼𝑥))
67 prid2g 4240 . . . . . . . . . . . . . 14 (𝑁𝑉𝑁 ∈ {𝐵, 𝑁})
6867ad2antrr 758 . . . . . . . . . . . . 13 (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → 𝑁 ∈ {𝐵, 𝑁})
6968adantl 481 . . . . . . . . . . . 12 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ {𝐵, 𝑁})
70 eleq2 2677 . . . . . . . . . . . 12 ((𝐼𝑦) = {𝐵, 𝑁} → (𝑁 ∈ (𝐼𝑦) ↔ 𝑁 ∈ {𝐵, 𝑁}))
7169, 70syl5ibr 235 . . . . . . . . . . 11 ((𝐼𝑦) = {𝐵, 𝑁} → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ (𝐼𝑦)))
7271adantl 481 . . . . . . . . . 10 (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ (𝐼𝑦)))
7372impcom 445 . . . . . . . . 9 ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑁 ∈ (𝐼𝑦))
7459, 66, 733jca 1235 . . . . . . . 8 ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → (𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦)))
7574ex 449 . . . . . . 7 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
7675reximdv 2999 . . . . . 6 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (∃𝑦 ∈ dom 𝐼((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → ∃𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
7776reximdv 2999 . . . . 5 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → ∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
7834, 77syl5bir 232 . . . 4 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → ((∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁}) → ∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
7933, 78sylbid 229 . . 3 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) → ∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
8079imp 444 . 2 ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦)))
8110, 80syl 17 1 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∃wrex 2897  {cpr 4127  dom cdm 5038  ran crn 5039  Fun wfun 5798   Fn wfn 5799  ‘cfv 5804  Vtxcvtx 25673  iEdgciedg 25674   UHGraph cuhgr 25722  Edgcedga 25792 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-sep 4709  ax-nul 4717  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  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-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-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-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-uhgr 25724  df-edga 25793 This theorem is referenced by:  umgr2edg  40436
 Copyright terms: Public domain W3C validator