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

Theorem uhgr2edg 27097
 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 1194 . . 3 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐺 ∈ UHGraph)
2 simp1r 1195 . . 3 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐴𝐵)
3 simp23 1205 . . . 4 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝑁𝑉)
4 simp21 1203 . . . 4 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐴𝑉)
5 3simpc 1147 . . . . 5 ((𝐴𝑉𝐵𝑉𝑁𝑉) → (𝐵𝑉𝑁𝑉))
653ad2ant2 1131 . . . 4 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → (𝐵𝑉𝑁𝑉))
73, 4, 6jca31 518 . . 3 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)))
81, 2, 7jca31 518 . 2 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))))
9 simp3 1135 . 2 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸))
10 usgrf1oedg.e . . . . . . . . 9 𝐸 = (Edg‘𝐺)
1110a1i 11 . . . . . . . 8 (𝐺 ∈ UHGraph → 𝐸 = (Edg‘𝐺))
12 edgval 26941 . . . . . . . . 9 (Edg‘𝐺) = ran (iEdg‘𝐺)
1312a1i 11 . . . . . . . 8 (𝐺 ∈ UHGraph → (Edg‘𝐺) = ran (iEdg‘𝐺))
14 usgrf1oedg.i . . . . . . . . . . 11 𝐼 = (iEdg‘𝐺)
1514eqcomi 2767 . . . . . . . . . 10 (iEdg‘𝐺) = 𝐼
1615a1i 11 . . . . . . . . 9 (𝐺 ∈ UHGraph → (iEdg‘𝐺) = 𝐼)
1716rneqd 5779 . . . . . . . 8 (𝐺 ∈ UHGraph → ran (iEdg‘𝐺) = ran 𝐼)
1811, 13, 173eqtrd 2797 . . . . . . 7 (𝐺 ∈ UHGraph → 𝐸 = ran 𝐼)
1918eleq2d 2837 . . . . . 6 (𝐺 ∈ UHGraph → ({𝑁, 𝐴} ∈ 𝐸 ↔ {𝑁, 𝐴} ∈ ran 𝐼))
2018eleq2d 2837 . . . . . 6 (𝐺 ∈ UHGraph → ({𝐵, 𝑁} ∈ 𝐸 ↔ {𝐵, 𝑁} ∈ ran 𝐼))
2119, 20anbi12d 633 . . . . 5 (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ ({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼)))
2214uhgrfun 26958 . . . . . . 7 (𝐺 ∈ UHGraph → Fun 𝐼)
2322funfnd 6366 . . . . . 6 (𝐺 ∈ UHGraph → 𝐼 Fn dom 𝐼)
24 fvelrnb 6714 . . . . . . 7 (𝐼 Fn dom 𝐼 → ({𝑁, 𝐴} ∈ ran 𝐼 ↔ ∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴}))
25 fvelrnb 6714 . . . . . . 7 (𝐼 Fn dom 𝐼 → ({𝐵, 𝑁} ∈ ran 𝐼 ↔ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁}))
2624, 25anbi12d 633 . . . . . 6 (𝐼 Fn dom 𝐼 → (({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁})))
2723, 26syl 17 . . . . 5 (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁})))
2821, 27bitrd 282 . . . 4 (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁})))
2928ad2antrr 725 . . 3 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁})))
30 reeanv 3285 . . . 4 (∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁}))
31 fveqeq2 6667 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝐼𝑥) = {𝑁, 𝐴} ↔ (𝐼𝑦) = {𝑁, 𝐴}))
3231anbi1d 632 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) ↔ ((𝐼𝑦) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})))
33 eqtr2 2779 . . . . . . . . . . . 12 (((𝐼𝑦) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → {𝑁, 𝐴} = {𝐵, 𝑁})
34 prcom 4625 . . . . . . . . . . . . . 14 {𝐵, 𝑁} = {𝑁, 𝐵}
3534eqeq2i 2771 . . . . . . . . . . . . 13 ({𝑁, 𝐴} = {𝐵, 𝑁} ↔ {𝑁, 𝐴} = {𝑁, 𝐵})
36 preq12bg 4741 . . . . . . . . . . . . . . . . 17 (((𝑁𝑉𝐴𝑉) ∧ (𝑁𝑉𝐵𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} ↔ ((𝑁 = 𝑁𝐴 = 𝐵) ∨ (𝑁 = 𝐵𝐴 = 𝑁))))
3736ancom2s 649 . . . . . . . . . . . . . . . 16 (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} ↔ ((𝑁 = 𝑁𝐴 = 𝐵) ∨ (𝑁 = 𝐵𝐴 = 𝑁))))
38 eqneqall 2962 . . . . . . . . . . . . . . . . . . 19 (𝐴 = 𝐵 → (𝐴𝐵𝑥𝑦))
3938adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝑁 = 𝑁𝐴 = 𝐵) → (𝐴𝐵𝑥𝑦))
40 eqtr 2778 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 = 𝑁𝑁 = 𝐵) → 𝐴 = 𝐵)
4140ancoms 462 . . . . . . . . . . . . . . . . . . 19 ((𝑁 = 𝐵𝐴 = 𝑁) → 𝐴 = 𝐵)
4241, 38syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑁 = 𝐵𝐴 = 𝑁) → (𝐴𝐵𝑥𝑦))
4339, 42jaoi 854 . . . . . . . . . . . . . . . . 17 (((𝑁 = 𝑁𝐴 = 𝐵) ∨ (𝑁 = 𝐵𝐴 = 𝑁)) → (𝐴𝐵𝑥𝑦))
4443adantld 494 . . . . . . . . . . . . . . . 16 (((𝑁 = 𝑁𝐴 = 𝐵) ∨ (𝑁 = 𝐵𝐴 = 𝑁)) → ((𝐺 ∈ UHGraph ∧ 𝐴𝐵) → 𝑥𝑦))
4537, 44syl6bi 256 . . . . . . . . . . . . . . 15 (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} → ((𝐺 ∈ UHGraph ∧ 𝐴𝐵) → 𝑥𝑦)))
4645com3l 89 . . . . . . . . . . . . . 14 ({𝑁, 𝐴} = {𝑁, 𝐵} → ((𝐺 ∈ UHGraph ∧ 𝐴𝐵) → (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → 𝑥𝑦)))
4746impd 414 . . . . . . . . . . . . 13 ({𝑁, 𝐴} = {𝑁, 𝐵} → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑥𝑦))
4835, 47sylbi 220 . . . . . . . . . . . 12 ({𝑁, 𝐴} = {𝐵, 𝑁} → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑥𝑦))
4933, 48syl 17 . . . . . . . . . . 11 (((𝐼𝑦) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑥𝑦))
5032, 49syl6bi 256 . . . . . . . . . 10 (𝑥 = 𝑦 → (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑥𝑦)))
5150impcomd 415 . . . . . . . . 9 (𝑥 = 𝑦 → ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑥𝑦))
52 ax-1 6 . . . . . . . . 9 (𝑥𝑦 → ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑥𝑦))
5351, 52pm2.61ine 3034 . . . . . . . 8 ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑥𝑦)
54 prid1g 4653 . . . . . . . . . . . . 13 (𝑁𝑉𝑁 ∈ {𝑁, 𝐴})
5554ad2antrr 725 . . . . . . . . . . . 12 (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → 𝑁 ∈ {𝑁, 𝐴})
5655adantl 485 . . . . . . . . . . 11 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ {𝑁, 𝐴})
57 eleq2 2840 . . . . . . . . . . 11 ((𝐼𝑥) = {𝑁, 𝐴} → (𝑁 ∈ (𝐼𝑥) ↔ 𝑁 ∈ {𝑁, 𝐴}))
5856, 57syl5ibr 249 . . . . . . . . . 10 ((𝐼𝑥) = {𝑁, 𝐴} → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ (𝐼𝑥)))
5958adantr 484 . . . . . . . . 9 (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ (𝐼𝑥)))
6059impcom 411 . . . . . . . 8 ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑁 ∈ (𝐼𝑥))
61 prid2g 4654 . . . . . . . . . . . . 13 (𝑁𝑉𝑁 ∈ {𝐵, 𝑁})
6261ad2antrr 725 . . . . . . . . . . . 12 (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → 𝑁 ∈ {𝐵, 𝑁})
6362adantl 485 . . . . . . . . . . 11 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ {𝐵, 𝑁})
64 eleq2 2840 . . . . . . . . . . 11 ((𝐼𝑦) = {𝐵, 𝑁} → (𝑁 ∈ (𝐼𝑦) ↔ 𝑁 ∈ {𝐵, 𝑁}))
6563, 64syl5ibr 249 . . . . . . . . . 10 ((𝐼𝑦) = {𝐵, 𝑁} → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ (𝐼𝑦)))
6665adantl 485 . . . . . . . . 9 (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ (𝐼𝑦)))
6766impcom 411 . . . . . . . 8 ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑁 ∈ (𝐼𝑦))
6853, 60, 673jca 1125 . . . . . . 7 ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → (𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦)))
6968ex 416 . . . . . 6 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
7069reximdv 3197 . . . . 5 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (∃𝑦 ∈ dom 𝐼((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → ∃𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
7170reximdv 3197 . . . 4 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → ∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
7230, 71syl5bir 246 . . 3 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → ((∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁}) → ∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
7329, 72sylbid 243 . 2 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) → ∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
748, 9, 73sylc 65 1 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  ∃wrex 3071  {cpr 4524  dom cdm 5524  ran crn 5525   Fn wfn 6330  ‘cfv 6335  Vtxcvtx 26888  iEdgciedg 26889  Edgcedg 26939  UHGraphcuhgr 26948 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298  ax-un 7459 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3697  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-fv 6343  df-edg 26940  df-uhgr 26950 This theorem is referenced by:  umgr2edg  27098
 Copyright terms: Public domain W3C validator