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

Theorem uhgr2edg 26905
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 1191 . . 3 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐺 ∈ UHGraph)
2 simp1r 1192 . . 3 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐴𝐵)
3 simp23 1202 . . . 4 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝑁𝑉)
4 simp21 1200 . . . 4 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐴𝑉)
5 3simpc 1144 . . . . 5 ((𝐴𝑉𝐵𝑉𝑁𝑉) → (𝐵𝑉𝑁𝑉))
653ad2ant2 1128 . . . 4 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → (𝐵𝑉𝑁𝑉))
73, 4, 6jca31 515 . . 3 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)))
81, 2, 7jca31 515 . 2 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))))
9 simp3 1132 . 2 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸))
10 usgrf1oedg.e . . . . . . . . 9 𝐸 = (Edg‘𝐺)
1110a1i 11 . . . . . . . 8 (𝐺 ∈ UHGraph → 𝐸 = (Edg‘𝐺))
12 edgval 26749 . . . . . . . . 9 (Edg‘𝐺) = ran (iEdg‘𝐺)
1312a1i 11 . . . . . . . 8 (𝐺 ∈ UHGraph → (Edg‘𝐺) = ran (iEdg‘𝐺))
14 usgrf1oedg.i . . . . . . . . . . 11 𝐼 = (iEdg‘𝐺)
1514eqcomi 2833 . . . . . . . . . 10 (iEdg‘𝐺) = 𝐼
1615a1i 11 . . . . . . . . 9 (𝐺 ∈ UHGraph → (iEdg‘𝐺) = 𝐼)
1716rneqd 5806 . . . . . . . 8 (𝐺 ∈ UHGraph → ran (iEdg‘𝐺) = ran 𝐼)
1811, 13, 173eqtrd 2864 . . . . . . 7 (𝐺 ∈ UHGraph → 𝐸 = ran 𝐼)
1918eleq2d 2902 . . . . . 6 (𝐺 ∈ UHGraph → ({𝑁, 𝐴} ∈ 𝐸 ↔ {𝑁, 𝐴} ∈ ran 𝐼))
2018eleq2d 2902 . . . . . 6 (𝐺 ∈ UHGraph → ({𝐵, 𝑁} ∈ 𝐸 ↔ {𝐵, 𝑁} ∈ ran 𝐼))
2119, 20anbi12d 630 . . . . 5 (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ ({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼)))
2214uhgrfun 26766 . . . . . . 7 (𝐺 ∈ UHGraph → Fun 𝐼)
2322funfnd 6382 . . . . . 6 (𝐺 ∈ UHGraph → 𝐼 Fn dom 𝐼)
24 fvelrnb 6722 . . . . . . 7 (𝐼 Fn dom 𝐼 → ({𝑁, 𝐴} ∈ ran 𝐼 ↔ ∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴}))
25 fvelrnb 6722 . . . . . . 7 (𝐼 Fn dom 𝐼 → ({𝐵, 𝑁} ∈ ran 𝐼 ↔ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁}))
2624, 25anbi12d 630 . . . . . 6 (𝐼 Fn dom 𝐼 → (({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁})))
2723, 26syl 17 . . . . 5 (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁})))
2821, 27bitrd 280 . . . 4 (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁})))
2928ad2antrr 722 . . 3 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁})))
30 reeanv 3372 . . . 4 (∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) ↔ (∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁}))
31 fveqeq2 6675 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝐼𝑥) = {𝑁, 𝐴} ↔ (𝐼𝑦) = {𝑁, 𝐴}))
3231anbi1d 629 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) ↔ ((𝐼𝑦) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})))
33 eqtr2 2846 . . . . . . . . . . . 12 (((𝐼𝑦) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → {𝑁, 𝐴} = {𝐵, 𝑁})
34 prcom 4666 . . . . . . . . . . . . . 14 {𝐵, 𝑁} = {𝑁, 𝐵}
3534eqeq2i 2837 . . . . . . . . . . . . 13 ({𝑁, 𝐴} = {𝐵, 𝑁} ↔ {𝑁, 𝐴} = {𝑁, 𝐵})
36 preq12bg 4782 . . . . . . . . . . . . . . . . 17 (((𝑁𝑉𝐴𝑉) ∧ (𝑁𝑉𝐵𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} ↔ ((𝑁 = 𝑁𝐴 = 𝐵) ∨ (𝑁 = 𝐵𝐴 = 𝑁))))
3736ancom2s 646 . . . . . . . . . . . . . . . 16 (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} ↔ ((𝑁 = 𝑁𝐴 = 𝐵) ∨ (𝑁 = 𝐵𝐴 = 𝑁))))
38 eqneqall 3031 . . . . . . . . . . . . . . . . . . 19 (𝐴 = 𝐵 → (𝐴𝐵𝑥𝑦))
3938adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑁 = 𝑁𝐴 = 𝐵) → (𝐴𝐵𝑥𝑦))
40 eqtr 2845 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 = 𝑁𝑁 = 𝐵) → 𝐴 = 𝐵)
4140ancoms 459 . . . . . . . . . . . . . . . . . . 19 ((𝑁 = 𝐵𝐴 = 𝑁) → 𝐴 = 𝐵)
4241, 38syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑁 = 𝐵𝐴 = 𝑁) → (𝐴𝐵𝑥𝑦))
4339, 42jaoi 853 . . . . . . . . . . . . . . . . 17 (((𝑁 = 𝑁𝐴 = 𝐵) ∨ (𝑁 = 𝐵𝐴 = 𝑁)) → (𝐴𝐵𝑥𝑦))
4443adantld 491 . . . . . . . . . . . . . . . 16 (((𝑁 = 𝑁𝐴 = 𝐵) ∨ (𝑁 = 𝐵𝐴 = 𝑁)) → ((𝐺 ∈ UHGraph ∧ 𝐴𝐵) → 𝑥𝑦))
4537, 44syl6bi 254 . . . . . . . . . . . . . . 15 (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} → ((𝐺 ∈ UHGraph ∧ 𝐴𝐵) → 𝑥𝑦)))
4645com3l 89 . . . . . . . . . . . . . 14 ({𝑁, 𝐴} = {𝑁, 𝐵} → ((𝐺 ∈ UHGraph ∧ 𝐴𝐵) → (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → 𝑥𝑦)))
4746impd 411 . . . . . . . . . . . . 13 ({𝑁, 𝐴} = {𝑁, 𝐵} → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑥𝑦))
4835, 47sylbi 218 . . . . . . . . . . . 12 ({𝑁, 𝐴} = {𝐵, 𝑁} → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑥𝑦))
4933, 48syl 17 . . . . . . . . . . 11 (((𝐼𝑦) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑥𝑦))
5032, 49syl6bi 254 . . . . . . . . . 10 (𝑥 = 𝑦 → (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑥𝑦)))
5150impcomd 412 . . . . . . . . 9 (𝑥 = 𝑦 → ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑥𝑦))
52 ax-1 6 . . . . . . . . 9 (𝑥𝑦 → ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑥𝑦))
5351, 52pm2.61ine 3104 . . . . . . . 8 ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑥𝑦)
54 prid1g 4694 . . . . . . . . . . . . 13 (𝑁𝑉𝑁 ∈ {𝑁, 𝐴})
5554ad2antrr 722 . . . . . . . . . . . 12 (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → 𝑁 ∈ {𝑁, 𝐴})
5655adantl 482 . . . . . . . . . . 11 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ {𝑁, 𝐴})
57 eleq2 2905 . . . . . . . . . . 11 ((𝐼𝑥) = {𝑁, 𝐴} → (𝑁 ∈ (𝐼𝑥) ↔ 𝑁 ∈ {𝑁, 𝐴}))
5856, 57syl5ibr 247 . . . . . . . . . 10 ((𝐼𝑥) = {𝑁, 𝐴} → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ (𝐼𝑥)))
5958adantr 481 . . . . . . . . 9 (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ (𝐼𝑥)))
6059impcom 408 . . . . . . . 8 ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑁 ∈ (𝐼𝑥))
61 prid2g 4695 . . . . . . . . . . . . 13 (𝑁𝑉𝑁 ∈ {𝐵, 𝑁})
6261ad2antrr 722 . . . . . . . . . . . 12 (((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉)) → 𝑁 ∈ {𝐵, 𝑁})
6362adantl 482 . . . . . . . . . . 11 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ {𝐵, 𝑁})
64 eleq2 2905 . . . . . . . . . . 11 ((𝐼𝑦) = {𝐵, 𝑁} → (𝑁 ∈ (𝐼𝑦) ↔ 𝑁 ∈ {𝐵, 𝑁}))
6563, 64syl5ibr 247 . . . . . . . . . 10 ((𝐼𝑦) = {𝐵, 𝑁} → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ (𝐼𝑦)))
6665adantl 482 . . . . . . . . 9 (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → 𝑁 ∈ (𝐼𝑦)))
6766impcom 408 . . . . . . . 8 ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → 𝑁 ∈ (𝐼𝑦))
6853, 60, 673jca 1122 . . . . . . 7 ((((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) ∧ ((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁})) → (𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦)))
6968ex 413 . . . . . 6 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → (𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
7069reximdv 3277 . . . . 5 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (∃𝑦 ∈ dom 𝐼((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → ∃𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
7170reximdv 3277 . . . 4 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼((𝐼𝑥) = {𝑁, 𝐴} ∧ (𝐼𝑦) = {𝐵, 𝑁}) → ∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
7230, 71syl5bir 244 . . 3 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → ((∃𝑥 ∈ dom 𝐼(𝐼𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼𝑦) = {𝐵, 𝑁}) → ∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
7329, 72sylbid 241 . 2 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ ((𝑁𝑉𝐴𝑉) ∧ (𝐵𝑉𝑁𝑉))) → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) → ∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦))))
748, 9, 73sylc 65 1 (((𝐺 ∈ UHGraph ∧ 𝐴𝐵) ∧ (𝐴𝑉𝐵𝑉𝑁𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼(𝑥𝑦𝑁 ∈ (𝐼𝑥) ∧ 𝑁 ∈ (𝐼𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wo 843  w3a 1081   = wceq 1530  wcel 2106  wne 3020  wrex 3143  {cpr 4565  dom cdm 5553  ran crn 5554   Fn wfn 6346  cfv 6351  Vtxcvtx 26696  iEdgciedg 26697  Edgcedg 26747  UHGraphcuhgr 26756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2615  df-eu 2649  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-rab 3151  df-v 3501  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4837  df-br 5063  df-opab 5125  df-mpt 5143  df-id 5458  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-fv 6359  df-edg 26748  df-uhgr 26758
This theorem is referenced by:  umgr2edg  26906
  Copyright terms: Public domain W3C validator