This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem upgrex

Description: An edge is an unordered pair of vertices. (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by AV, 10-Oct-2020)

Ref Expression
Hypotheses isupgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isupgr.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion upgrex ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } )

Proof

Step Hyp Ref Expression
1 isupgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isupgr.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3 1 2 upgrn0 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) → ( 𝐸 ‘ 𝐹 ) ≠ ∅ )
4 n0 ⊢ ( ( 𝐸 ‘ 𝐹 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) )
5 3 4 sylib ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) → ∃ 𝑥 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) )
6 simp1 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) → 𝐺 ∈ UPGraph )
7 fndm ⊢ ( 𝐸 Fn 𝐴 → dom 𝐸 = 𝐴 )
8 7 eqcomd ⊢ ( 𝐸 Fn 𝐴 → 𝐴 = dom 𝐸 )
9 8 eleq2d ⊢ ( 𝐸 Fn 𝐴 → ( 𝐹 ∈ 𝐴 ↔ 𝐹 ∈ dom 𝐸 ) )
10 9 biimpd ⊢ ( 𝐸 Fn 𝐴 → ( 𝐹 ∈ 𝐴 → 𝐹 ∈ dom 𝐸 ) )
11 10 a1i ⊢ ( 𝐺 ∈ UPGraph → ( 𝐸 Fn 𝐴 → ( 𝐹 ∈ 𝐴 → 𝐹 ∈ dom 𝐸 ) ) )
12 11 3imp ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) → 𝐹 ∈ dom 𝐸 )
13 1 2 upgrss ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝐹 ) ⊆ 𝑉 )
14 6 12 13 syl2anc ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) → ( 𝐸 ‘ 𝐹 ) ⊆ 𝑉 )
15 14 sselda ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ) → 𝑥 ∈ 𝑉 )
16 15 adantr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ) ∧ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) = ∅ ) → 𝑥 ∈ 𝑉 )
17 simpr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ) ∧ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) = ∅ ) → ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) = ∅ )
18 ssdif0 ⊢ ( ( 𝐸 ‘ 𝐹 ) ⊆ { 𝑥 } ↔ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) = ∅ )
19 17 18 sylibr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ) ∧ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) = ∅ ) → ( 𝐸 ‘ 𝐹 ) ⊆ { 𝑥 } )
20 simpr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ) → 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) )
21 20 snssd ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ) → { 𝑥 } ⊆ ( 𝐸 ‘ 𝐹 ) )
22 21 adantr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ) ∧ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) = ∅ ) → { 𝑥 } ⊆ ( 𝐸 ‘ 𝐹 ) )
23 19 22 eqssd ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ) ∧ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) = ∅ ) → ( 𝐸 ‘ 𝐹 ) = { 𝑥 } )
24 preq2 ⊢ ( 𝑦 = 𝑥 → { 𝑥 , 𝑦 } = { 𝑥 , 𝑥 } )
25 dfsn2 ⊢ { 𝑥 } = { 𝑥 , 𝑥 }
26 24 25 eqtr4di ⊢ ( 𝑦 = 𝑥 → { 𝑥 , 𝑦 } = { 𝑥 } )
27 26 rspceeqv ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝐸 ‘ 𝐹 ) = { 𝑥 } ) → ∃ 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } )
28 16 23 27 syl2anc ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ) ∧ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) = ∅ ) → ∃ 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } )
29 n0 ⊢ ( ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) )
30 14 adantr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ∧ 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) ) → ( 𝐸 ‘ 𝐹 ) ⊆ 𝑉 )
31 simprr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ∧ 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) ) → 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) )
32 31 eldifad ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ∧ 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) ) → 𝑦 ∈ ( 𝐸 ‘ 𝐹 ) )
33 30 32 sseldd ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ∧ 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) ) → 𝑦 ∈ 𝑉 )
34 1 2 upgrfi ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) → ( 𝐸 ‘ 𝐹 ) ∈ Fin )
35 34 adantr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ∧ 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) ) → ( 𝐸 ‘ 𝐹 ) ∈ Fin )
36 simprl ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ∧ 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) ) → 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) )
37 36 32 prssd ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ∧ 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) ) → { 𝑥 , 𝑦 } ⊆ ( 𝐸 ‘ 𝐹 ) )
38 fvex ⊢ ( 𝐸 ‘ 𝐹 ) ∈ V
39 ssdomg ⊢ ( ( 𝐸 ‘ 𝐹 ) ∈ V → ( { 𝑥 , 𝑦 } ⊆ ( 𝐸 ‘ 𝐹 ) → { 𝑥 , 𝑦 } ≼ ( 𝐸 ‘ 𝐹 ) ) )
40 38 37 39 mpsyl ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ∧ 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) ) → { 𝑥 , 𝑦 } ≼ ( 𝐸 ‘ 𝐹 ) )
41 1 2 upgrle ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐸 ‘ 𝐹 ) ) ≤ 2 )
42 41 adantr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ∧ 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) ) → ( ♯ ‘ ( 𝐸 ‘ 𝐹 ) ) ≤ 2 )
43 eldifsni ⊢ ( 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) → 𝑦 ≠ 𝑥 )
44 43 ad2antll ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ∧ 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) ) → 𝑦 ≠ 𝑥 )
45 44 necomd ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ∧ 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) ) → 𝑥 ≠ 𝑦 )
46 hashprg ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ≠ 𝑦 ↔ ( ♯ ‘ { 𝑥 , 𝑦 } ) = 2 ) )
47 46 el2v ⊢ ( 𝑥 ≠ 𝑦 ↔ ( ♯ ‘ { 𝑥 , 𝑦 } ) = 2 )
48 45 47 sylib ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ∧ 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) ) → ( ♯ ‘ { 𝑥 , 𝑦 } ) = 2 )
49 42 48 breqtrrd ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ∧ 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) ) → ( ♯ ‘ ( 𝐸 ‘ 𝐹 ) ) ≤ ( ♯ ‘ { 𝑥 , 𝑦 } ) )
50 prfi ⊢ { 𝑥 , 𝑦 } ∈ Fin
51 hashdom ⊢ ( ( ( 𝐸 ‘ 𝐹 ) ∈ Fin ∧ { 𝑥 , 𝑦 } ∈ Fin ) → ( ( ♯ ‘ ( 𝐸 ‘ 𝐹 ) ) ≤ ( ♯ ‘ { 𝑥 , 𝑦 } ) ↔ ( 𝐸 ‘ 𝐹 ) ≼ { 𝑥 , 𝑦 } ) )
52 35 50 51 sylancl ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ∧ 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) ) → ( ( ♯ ‘ ( 𝐸 ‘ 𝐹 ) ) ≤ ( ♯ ‘ { 𝑥 , 𝑦 } ) ↔ ( 𝐸 ‘ 𝐹 ) ≼ { 𝑥 , 𝑦 } ) )
53 49 52 mpbid ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ∧ 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) ) → ( 𝐸 ‘ 𝐹 ) ≼ { 𝑥 , 𝑦 } )
54 sbth ⊢ ( ( { 𝑥 , 𝑦 } ≼ ( 𝐸 ‘ 𝐹 ) ∧ ( 𝐸 ‘ 𝐹 ) ≼ { 𝑥 , 𝑦 } ) → { 𝑥 , 𝑦 } ≈ ( 𝐸 ‘ 𝐹 ) )
55 40 53 54 syl2anc ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ∧ 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) ) → { 𝑥 , 𝑦 } ≈ ( 𝐸 ‘ 𝐹 ) )
56 fisseneq ⊢ ( ( ( 𝐸 ‘ 𝐹 ) ∈ Fin ∧ { 𝑥 , 𝑦 } ⊆ ( 𝐸 ‘ 𝐹 ) ∧ { 𝑥 , 𝑦 } ≈ ( 𝐸 ‘ 𝐹 ) ) → { 𝑥 , 𝑦 } = ( 𝐸 ‘ 𝐹 ) )
57 35 37 55 56 syl3anc ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ∧ 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) ) → { 𝑥 , 𝑦 } = ( 𝐸 ‘ 𝐹 ) )
58 57 eqcomd ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ∧ 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) ) → ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } )
59 33 58 jca ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ∧ 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) ) → ( 𝑦 ∈ 𝑉 ∧ ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } ) )
60 59 expr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ) → ( 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) → ( 𝑦 ∈ 𝑉 ∧ ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } ) ) )
61 60 eximdv ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ) → ( ∃ 𝑦 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) → ∃ 𝑦 ( 𝑦 ∈ 𝑉 ∧ ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } ) ) )
62 61 imp ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ) ∧ ∃ 𝑦 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) → ∃ 𝑦 ( 𝑦 ∈ 𝑉 ∧ ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } ) )
63 df-rex ⊢ ( ∃ 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑉 ∧ ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } ) )
64 62 63 sylibr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ) ∧ ∃ 𝑦 𝑦 ∈ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ) → ∃ 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } )
65 29 64 sylan2b ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ) ∧ ( ( 𝐸 ‘ 𝐹 ) ∖ { 𝑥 } ) ≠ ∅ ) → ∃ 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } )
66 28 65 pm2.61dane ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ) → ∃ 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } )
67 15 66 jca ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) ) → ( 𝑥 ∈ 𝑉 ∧ ∃ 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } ) )
68 67 ex ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) → ( 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) → ( 𝑥 ∈ 𝑉 ∧ ∃ 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } ) ) )
69 68 eximdv ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) → ( ∃ 𝑥 𝑥 ∈ ( 𝐸 ‘ 𝐹 ) → ∃ 𝑥 ( 𝑥 ∈ 𝑉 ∧ ∃ 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } ) ) )
70 5 69 mpd ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) → ∃ 𝑥 ( 𝑥 ∈ 𝑉 ∧ ∃ 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } ) )
71 df-rex ⊢ ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑉 ∧ ∃ 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } ) )
72 70 71 sylibr ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝐹 ) = { 𝑥 , 𝑦 } )