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

Theorem uhgr2edg 25987
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 1083 . . . 4 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐺 ∈ UHGraph )
2 simp1r 1084 . . . 4 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐴𝐵)
3 simp23 1094 . . . . 5 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝑁𝑉)
4 simp21 1092 . . . . 5 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐴𝑉)
5 3simpc 1058 . . . . . 6 ((𝐴𝑉𝐵𝑉𝑁𝑉) → (𝐵𝑉𝑁𝑉))
653ad2ant2 1081 . . . . 5 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → (𝐵𝑉𝑁𝑉))
73, 4, 6jca31 556 . . . 4 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)))
81, 2, 7jca31 556 . . 3 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))))
9 simp3 1061 . . 3 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸))
108, 9jca 554 . 2 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)))
11 usgrf1oedg.e . . . . . . . . . 10 𝐸 = (Edg‘𝐺)
1211a1i 11 . . . . . . . . 9 (𝐺 ∈ UHGraph → 𝐸 = (Edg‘𝐺))
13 edgval 25836 . . . . . . . . 9 (𝐺 ∈ UHGraph → (Edg‘𝐺) = ran (iEdg‘𝐺))
14 usgrf1oedg.i . . . . . . . . . . . 12 𝐼 = (iEdg‘𝐺)
1514eqcomi 2635 . . . . . . . . . . 11 (iEdg‘𝐺) = 𝐼
1615a1i 11 . . . . . . . . . 10 (𝐺 ∈ UHGraph → (iEdg‘𝐺) = 𝐼)
1716rneqd 5317 . . . . . . . . 9 (𝐺 ∈ UHGraph → ran (iEdg‘𝐺) = ran 𝐼)
1812, 13, 173eqtrd 2664 . . . . . . . 8 (𝐺 ∈ UHGraph → 𝐸 = ran 𝐼)
1918eleq2d 2689 . . . . . . 7 (𝐺 ∈ UHGraph → ({𝑁, 𝐴} ∈ 𝐸 ↔ {𝑁, 𝐴} ∈ ran 𝐼))
2018eleq2d 2689 . . . . . . 7 (𝐺 ∈ UHGraph → ({𝐵, 𝑁} ∈ 𝐸 ↔ {𝐵, 𝑁} ∈ ran 𝐼))
2119, 20anbi12d 746 . . . . . 6 (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ ({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼)))
22 eqid 2626 . . . . . . . . . 10 (iEdg‘𝐺) = (iEdg‘𝐺)
2322uhgrfun 25852 . . . . . . . . 9 (𝐺 ∈ UHGraph → Fun (iEdg‘𝐺))
2414funeqi 5870 . . . . . . . . 9 (Fun 𝐼 ↔ Fun (iEdg‘𝐺))
2523, 24sylibr 224 . . . . . . . 8 (𝐺 ∈ UHGraph → Fun 𝐼)
26 funfn 5879 . . . . . . . 8 (Fun 𝐼𝐼 Fn dom 𝐼)
2725, 26sylib 208 . . . . . . 7 (𝐺 ∈ UHGraph → 𝐼 Fn dom 𝐼)
28 fvelrnb 6201 . . . . . . . 8 (𝐼 Fn dom 𝐼 → ({𝑁, 𝐴} ∈ ran 𝐼 ↔ ∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴}))
29 fvelrnb 6201 . . . . . . . 8 (𝐼 Fn dom 𝐼 → ({𝐵, 𝑁} ∈ ran 𝐼 ↔ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁}))
3028, 29anbi12d 746 . . . . . . 7 (𝐼 Fn dom 𝐼 → (({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁})))
3127, 30syl 17 . . . . . 6 (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁})))
3221, 31bitrd 268 . . . . 5 (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁})))
3332ad2antrr 761 . . . 4 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁})))
34 reeanv 3102 . . . . 5 (∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁}))
35 fveq2 6150 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝐼𝑥) = (𝐼𝑦))
3635eqeq1d 2628 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝐼𝑥) = {𝑁, 𝐴} ↔ (𝐼𝑦) = {𝑁, 𝐴}))
3736anbi1d 740 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) ↔ ((𝐼𝑦) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})))
38 eqtr2 2646 . . . . . . . . . . . . . 14 (((𝐼𝑦) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → {𝑁, 𝐴} = {𝐵, 𝑁})
39 prcom 4242 . . . . . . . . . . . . . . . 16 {𝐵, 𝑁} = {𝑁, 𝐵}
4039eqeq2i 2638 . . . . . . . . . . . . . . 15 ({𝑁, 𝐴} = {𝐵, 𝑁} ↔ {𝑁, 𝐴} = {𝑁, 𝐵})
41 preq12bg 4359 . . . . . . . . . . . . . . . . . . 19 (((𝑁𝑉𝐴𝑉) ∧ (𝑁𝑉𝐵𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} ↔ ((𝑁 = 𝑁𝐴 = 𝐵) ∨ (𝑁 = 𝐵𝐴 = 𝑁))))
4241ancom2s 843 . . . . . . . . . . . . . . . . . 18 (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} ↔ ((𝑁 = 𝑁𝐴 = 𝐵) ∨ (𝑁 = 𝐵𝐴 = 𝑁))))
43 eqneqall 2807 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 = 𝐵 → (𝐴𝐵𝑥𝑦))
4443adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 = 𝑁𝐴 = 𝐵) → (𝐴𝐵𝑥𝑦))
45 eqtr 2645 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 = 𝑁𝑁 = 𝐵) → 𝐴 = 𝐵)
4645ancoms 469 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 = 𝐵𝐴 = 𝑁) → 𝐴 = 𝐵)
4746, 43syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 = 𝐵𝐴 = 𝑁) → (𝐴𝐵𝑥𝑦))
4844, 47jaoi 394 . . . . . . . . . . . . . . . . . . 19 (((𝑁 = 𝑁𝐴 = 𝐵) ∨ (𝑁 = 𝐵𝐴 = 𝑁)) → (𝐴𝐵𝑥𝑦))
4948adantld 483 . . . . . . . . . . . . . . . . . 18 (((𝑁 = 𝑁𝐴 = 𝐵) ∨ (𝑁 = 𝐵𝐴 = 𝑁)) → ((𝐺 ∈ UHGraph ∧ 𝐴𝐵) → 𝑥𝑦))
5042, 49syl6bi 243 . . . . . . . . . . . . . . . . 17 (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} → ((𝐺 ∈ UHGraph ∧ 𝐴𝐵) → 𝑥𝑦)))
5150com3l 89 . . . . . . . . . . . . . . . 16 ({𝑁, 𝐴} = {𝑁, 𝐵} → ((𝐺 ∈ UHGraph ∧ 𝐴𝐵) → (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → 𝑥𝑦)))
5251impd 447 . . . . . . . . . . . . . . 15 ({𝑁, 𝐴} = {𝑁, 𝐵} → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑥𝑦))
5340, 52sylbi 207 . . . . . . . . . . . . . 14 ({𝑁, 𝐴} = {𝐵, 𝑁} → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑥𝑦))
5438, 53syl 17 . . . . . . . . . . . . 13 (((𝐼𝑦) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑥𝑦))
5537, 54syl6bi 243 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑥𝑦)))
5655com23 86 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → 𝑥𝑦)))
5756impd 447 . . . . . . . . . 10 (𝑥 = 𝑦 → ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑥𝑦))
58 ax-1 6 . . . . . . . . . 10 (𝑥𝑦 → ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑥𝑦))
5957, 58pm2.61ine 2879 . . . . . . . . 9 ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑥𝑦)
60 prid1g 4270 . . . . . . . . . . . . . 14 (𝑁𝑉𝑁 ∈ {𝑁, 𝐴})
6160ad2antrr 761 . . . . . . . . . . . . 13 (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → 𝑁 ∈ {𝑁, 𝐴})
6261adantl 482 . . . . . . . . . . . 12 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ {𝑁, 𝐴})
63 eleq2 2693 . . . . . . . . . . . 12 ((𝐼𝑥) = {𝑁, 𝐴} → (𝑁 ∈ (𝐼𝑥) ↔ 𝑁 ∈ {𝑁, 𝐴}))
6462, 63syl5ibr 236 . . . . . . . . . . 11 ((𝐼𝑥) = {𝑁, 𝐴} → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ (𝐼𝑥)))
6564adantr 481 . . . . . . . . . 10 (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ (𝐼𝑥)))
6665impcom 446 . . . . . . . . 9 ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑁 ∈ (𝐼𝑥))
67 prid2g 4271 . . . . . . . . . . . . . 14 (𝑁𝑉𝑁 ∈ {𝐵, 𝑁})
6867ad2antrr 761 . . . . . . . . . . . . 13 (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → 𝑁 ∈ {𝐵, 𝑁})
6968adantl 482 . . . . . . . . . . . 12 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ {𝐵, 𝑁})
70 eleq2 2693 . . . . . . . . . . . 12 ((𝐼𝑦) = {𝐵, 𝑁} → (𝑁 ∈ (𝐼𝑦) ↔ 𝑁 ∈ {𝐵, 𝑁}))
7169, 70syl5ibr 236 . . . . . . . . . . 11 ((𝐼𝑦) = {𝐵, 𝑁} → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ (𝐼𝑦)))
7271adantl 482 . . . . . . . . . 10 (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ (𝐼𝑦)))
7372impcom 446 . . . . . . . . 9 ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑁 ∈ (𝐼𝑦))
7459, 66, 733jca 1240 . . . . . . . 8 ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → (𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦)))
7574ex 450 . . . . . . 7 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
7675reximdv 3015 . . . . . 6 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (∃𝑦 ∈ dom 𝐼((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → ∃𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
7776reximdv 3015 . . . . 5 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → ∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
7834, 77syl5bir 233 . . . 4 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → ((∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁}) → ∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
7933, 78sylbid 230 . . 3 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) → ∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
8079imp 445 . 2 ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦)))
8110, 80syl 17 1 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1480  wcel 1992  wne 2796  wrex 2913  {cpr 4155  dom cdm 5079  ran crn 5080  Fun wfun 5844   Fn wfn 5845  cfv 5850  Vtxcvtx 25769  iEdgciedg 25770  Edgcedg 25834   UHGraph cuhgr 25842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pr 4872  ax-un 6903
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-fv 5858  df-edg 25835  df-uhgr 25844
This theorem is referenced by:  umgr2edg  25988
  Copyright terms: Public domain W3C validator