Metamath Proof Explorer

Theorem 3vfriswmgrlem

Description: Lemma for 3vfriswmgr . (Contributed by Alexander van der Vekens, 6-Oct-2017) (Revised by AV, 31-Mar-2021)

Ref Expression
Hypotheses 3vfriswmgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
3vfriswmgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion 3vfriswmgrlem ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐴 , 𝐵 } ∈ 𝐸 → ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 3vfriswmgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 3vfriswmgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 animorr ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ( { 𝐴 , 𝐴 } ∈ 𝐸 ∨ { 𝐴 , 𝐵 } ∈ 𝐸 ) )
4 preq2 ⊢ ( 𝑤 = 𝐴 → { 𝐴 , 𝑤 } = { 𝐴 , 𝐴 } )
5 4 eleq1d ⊢ ( 𝑤 = 𝐴 → ( { 𝐴 , 𝑤 } ∈ 𝐸 ↔ { 𝐴 , 𝐴 } ∈ 𝐸 ) )
6 preq2 ⊢ ( 𝑤 = 𝐵 → { 𝐴 , 𝑤 } = { 𝐴 , 𝐵 } )
7 6 eleq1d ⊢ ( 𝑤 = 𝐵 → ( { 𝐴 , 𝑤 } ∈ 𝐸 ↔ { 𝐴 , 𝐵 } ∈ 𝐸 ) )
8 5 7 rexprg ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( ∃ 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 ↔ ( { 𝐴 , 𝐴 } ∈ 𝐸 ∨ { 𝐴 , 𝐵 } ∈ 𝐸 ) ) )
9 8 3adant3 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) → ( ∃ 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 ↔ ( { 𝐴 , 𝐴 } ∈ 𝐸 ∨ { 𝐴 , 𝐵 } ∈ 𝐸 ) ) )
10 9 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ( ∃ 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 ↔ ( { 𝐴 , 𝐴 } ∈ 𝐸 ∨ { 𝐴 , 𝐵 } ∈ 𝐸 ) ) )
11 3 10 mpbird ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ∃ 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 )
12 df-rex ⊢ ( ∃ 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 ↔ ∃ 𝑤 ( 𝑤 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝑤 } ∈ 𝐸 ) )
13 11 12 sylib ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ∃ 𝑤 ( 𝑤 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝑤 } ∈ 𝐸 ) )
14 vex ⊢ 𝑤 ∈ V
15 14 elpr ⊢ ( 𝑤 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) )
16 vex ⊢ 𝑦 ∈ V
17 16 elpr ⊢ ( 𝑦 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) )
18 eqidd ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 = 𝐴 )
19 18 a1i ⊢ ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 = 𝐴 ) )
20 19 a1i13 ⊢ ( 𝑦 = 𝐴 → ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 = 𝐴 ) ) ) )
21 preq2 ⊢ ( 𝑦 = 𝐴 → { 𝐴 , 𝑦 } = { 𝐴 , 𝐴 } )
22 21 eleq1d ⊢ ( 𝑦 = 𝐴 → ( { 𝐴 , 𝑦 } ∈ 𝐸 ↔ { 𝐴 , 𝐴 } ∈ 𝐸 ) )
23 eqeq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐴 = 𝑦 ↔ 𝐴 = 𝐴 ) )
24 23 imbi2d ⊢ ( 𝑦 = 𝐴 → ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 = 𝑦 ) ↔ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 = 𝐴 ) ) )
25 24 imbi2d ⊢ ( 𝑦 = 𝐴 → ( ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 = 𝑦 ) ) ↔ ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 = 𝐴 ) ) ) )
26 20 22 25 3imtr4d ⊢ ( 𝑦 = 𝐴 → ( { 𝐴 , 𝑦 } ∈ 𝐸 → ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 = 𝑦 ) ) ) )
27 2 usgredgne ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝐴 , 𝐴 } ∈ 𝐸 ) → 𝐴 ≠ 𝐴 )
28 27 adantll ⊢ ( ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ∧ { 𝐴 , 𝐴 } ∈ 𝐸 ) → 𝐴 ≠ 𝐴 )
29 df-ne ⊢ ( 𝐴 ≠ 𝐴 ↔ ¬ 𝐴 = 𝐴 )
30 eqid ⊢ 𝐴 = 𝐴
31 30 pm2.24i ⊢ ( ¬ 𝐴 = 𝐴 → 𝐴 = 𝐵 )
32 29 31 sylbi ⊢ ( 𝐴 ≠ 𝐴 → 𝐴 = 𝐵 )
33 28 32 syl ⊢ ( ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ∧ { 𝐴 , 𝐴 } ∈ 𝐸 ) → 𝐴 = 𝐵 )
34 33 ex ⊢ ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( { 𝐴 , 𝐴 } ∈ 𝐸 → 𝐴 = 𝐵 ) )
35 34 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ( { 𝐴 , 𝐴 } ∈ 𝐸 → 𝐴 = 𝐵 ) )
36 35 com12 ⊢ ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 = 𝐵 ) )
37 36 2a1i ⊢ ( 𝑦 = 𝐵 → ( { 𝐴 , 𝐵 } ∈ 𝐸 → ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 = 𝐵 ) ) ) )
38 preq2 ⊢ ( 𝑦 = 𝐵 → { 𝐴 , 𝑦 } = { 𝐴 , 𝐵 } )
39 38 eleq1d ⊢ ( 𝑦 = 𝐵 → ( { 𝐴 , 𝑦 } ∈ 𝐸 ↔ { 𝐴 , 𝐵 } ∈ 𝐸 ) )
40 eqeq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 = 𝑦 ↔ 𝐴 = 𝐵 ) )
41 40 imbi2d ⊢ ( 𝑦 = 𝐵 → ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 = 𝑦 ) ↔ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 = 𝐵 ) ) )
42 41 imbi2d ⊢ ( 𝑦 = 𝐵 → ( ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 = 𝑦 ) ) ↔ ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 = 𝐵 ) ) ) )
43 37 39 42 3imtr4d ⊢ ( 𝑦 = 𝐵 → ( { 𝐴 , 𝑦 } ∈ 𝐸 → ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 = 𝑦 ) ) ) )
44 26 43 jaoi ⊢ ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → ( { 𝐴 , 𝑦 } ∈ 𝐸 → ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 = 𝑦 ) ) ) )
45 eqeq1 ⊢ ( 𝑤 = 𝐴 → ( 𝑤 = 𝑦 ↔ 𝐴 = 𝑦 ) )
46 45 imbi2d ⊢ ( 𝑤 = 𝐴 → ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝑤 = 𝑦 ) ↔ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 = 𝑦 ) ) )
47 5 46 imbi12d ⊢ ( 𝑤 = 𝐴 → ( ( { 𝐴 , 𝑤 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝑤 = 𝑦 ) ) ↔ ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 = 𝑦 ) ) ) )
48 47 imbi2d ⊢ ( 𝑤 = 𝐴 → ( ( { 𝐴 , 𝑦 } ∈ 𝐸 → ( { 𝐴 , 𝑤 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝑤 = 𝑦 ) ) ) ↔ ( { 𝐴 , 𝑦 } ∈ 𝐸 → ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 = 𝑦 ) ) ) ) )
49 44 48 imbitrrid ⊢ ( 𝑤 = 𝐴 → ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → ( { 𝐴 , 𝑦 } ∈ 𝐸 → ( { 𝐴 , 𝑤 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝑤 = 𝑦 ) ) ) ) )
50 30 pm2.24i ⊢ ( ¬ 𝐴 = 𝐴 → 𝐵 = 𝐴 )
51 29 50 sylbi ⊢ ( 𝐴 ≠ 𝐴 → 𝐵 = 𝐴 )
52 28 51 syl ⊢ ( ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ∧ { 𝐴 , 𝐴 } ∈ 𝐸 ) → 𝐵 = 𝐴 )
53 52 ex ⊢ ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( { 𝐴 , 𝐴 } ∈ 𝐸 → 𝐵 = 𝐴 ) )
54 53 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ( { 𝐴 , 𝐴 } ∈ 𝐸 → 𝐵 = 𝐴 ) )
55 54 com12 ⊢ ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝐴 ) )
56 55 a1i13 ⊢ ( 𝑦 = 𝐴 → ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( { 𝐴 , 𝐵 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝐴 ) ) ) )
57 eqeq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐵 = 𝑦 ↔ 𝐵 = 𝐴 ) )
58 57 imbi2d ⊢ ( 𝑦 = 𝐴 → ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝑦 ) ↔ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝐴 ) ) )
59 58 imbi2d ⊢ ( 𝑦 = 𝐴 → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝑦 ) ) ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝐴 ) ) ) )
60 56 22 59 3imtr4d ⊢ ( 𝑦 = 𝐴 → ( { 𝐴 , 𝑦 } ∈ 𝐸 → ( { 𝐴 , 𝐵 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝑦 ) ) ) )
61 eqidd ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝐵 )
62 61 a1i ⊢ ( { 𝐴 , 𝐵 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝐵 ) )
63 62 a1i13 ⊢ ( 𝑦 = 𝐵 → ( { 𝐴 , 𝐵 } ∈ 𝐸 → ( { 𝐴 , 𝐵 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝐵 ) ) ) )
64 eqeq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐵 = 𝑦 ↔ 𝐵 = 𝐵 ) )
65 64 imbi2d ⊢ ( 𝑦 = 𝐵 → ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝑦 ) ↔ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝐵 ) ) )
66 65 imbi2d ⊢ ( 𝑦 = 𝐵 → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝑦 ) ) ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝐵 ) ) ) )
67 63 39 66 3imtr4d ⊢ ( 𝑦 = 𝐵 → ( { 𝐴 , 𝑦 } ∈ 𝐸 → ( { 𝐴 , 𝐵 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝑦 ) ) ) )
68 60 67 jaoi ⊢ ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → ( { 𝐴 , 𝑦 } ∈ 𝐸 → ( { 𝐴 , 𝐵 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝑦 ) ) ) )
69 eqeq1 ⊢ ( 𝑤 = 𝐵 → ( 𝑤 = 𝑦 ↔ 𝐵 = 𝑦 ) )
70 69 imbi2d ⊢ ( 𝑤 = 𝐵 → ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝑤 = 𝑦 ) ↔ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝑦 ) ) )
71 7 70 imbi12d ⊢ ( 𝑤 = 𝐵 → ( ( { 𝐴 , 𝑤 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝑤 = 𝑦 ) ) ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝑦 ) ) ) )
72 71 imbi2d ⊢ ( 𝑤 = 𝐵 → ( ( { 𝐴 , 𝑦 } ∈ 𝐸 → ( { 𝐴 , 𝑤 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝑤 = 𝑦 ) ) ) ↔ ( { 𝐴 , 𝑦 } ∈ 𝐸 → ( { 𝐴 , 𝐵 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝑦 ) ) ) ) )
73 68 72 imbitrrid ⊢ ( 𝑤 = 𝐵 → ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → ( { 𝐴 , 𝑦 } ∈ 𝐸 → ( { 𝐴 , 𝑤 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝑤 = 𝑦 ) ) ) ) )
74 49 73 jaoi ⊢ ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → ( { 𝐴 , 𝑦 } ∈ 𝐸 → ( { 𝐴 , 𝑤 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝑤 = 𝑦 ) ) ) ) )
75 74 com3l ⊢ ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) → ( { 𝐴 , 𝑦 } ∈ 𝐸 → ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → ( { 𝐴 , 𝑤 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝑤 = 𝑦 ) ) ) ) )
76 17 75 sylbi ⊢ ( 𝑦 ∈ { 𝐴 , 𝐵 } → ( { 𝐴 , 𝑦 } ∈ 𝐸 → ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → ( { 𝐴 , 𝑤 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝑤 = 𝑦 ) ) ) ) )
77 76 imp ⊢ ( ( 𝑦 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝑦 } ∈ 𝐸 ) → ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → ( { 𝐴 , 𝑤 } ∈ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝑤 = 𝑦 ) ) ) )
78 77 com3l ⊢ ( ( 𝑤 = 𝐴 ∨ 𝑤 = 𝐵 ) → ( { 𝐴 , 𝑤 } ∈ 𝐸 → ( ( 𝑦 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝑦 } ∈ 𝐸 ) → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝑤 = 𝑦 ) ) ) )
79 15 78 sylbi ⊢ ( 𝑤 ∈ { 𝐴 , 𝐵 } → ( { 𝐴 , 𝑤 } ∈ 𝐸 → ( ( 𝑦 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝑦 } ∈ 𝐸 ) → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝑤 = 𝑦 ) ) ) )
80 79 imp31 ⊢ ( ( ( 𝑤 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝑤 } ∈ 𝐸 ) ∧ ( 𝑦 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝑦 } ∈ 𝐸 ) ) → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝑤 = 𝑦 ) )
81 80 com12 ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ( ( ( 𝑤 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝑤 } ∈ 𝐸 ) ∧ ( 𝑦 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝑦 } ∈ 𝐸 ) ) → 𝑤 = 𝑦 ) )
82 81 alrimivv ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ∀ 𝑤 ∀ 𝑦 ( ( ( 𝑤 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝑤 } ∈ 𝐸 ) ∧ ( 𝑦 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝑦 } ∈ 𝐸 ) ) → 𝑤 = 𝑦 ) )
83 eleq1w ⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ { 𝐴 , 𝐵 } ↔ 𝑦 ∈ { 𝐴 , 𝐵 } ) )
84 preq2 ⊢ ( 𝑤 = 𝑦 → { 𝐴 , 𝑤 } = { 𝐴 , 𝑦 } )
85 84 eleq1d ⊢ ( 𝑤 = 𝑦 → ( { 𝐴 , 𝑤 } ∈ 𝐸 ↔ { 𝐴 , 𝑦 } ∈ 𝐸 ) )
86 83 85 anbi12d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝑤 } ∈ 𝐸 ) ↔ ( 𝑦 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝑦 } ∈ 𝐸 ) ) )
87 86 eu4 ⊢ ( ∃! 𝑤 ( 𝑤 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝑤 } ∈ 𝐸 ) ↔ ( ∃ 𝑤 ( 𝑤 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝑤 } ∈ 𝐸 ) ∧ ∀ 𝑤 ∀ 𝑦 ( ( ( 𝑤 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝑤 } ∈ 𝐸 ) ∧ ( 𝑦 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝑦 } ∈ 𝐸 ) ) → 𝑤 = 𝑦 ) ) )
88 13 82 87 sylanbrc ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ∃! 𝑤 ( 𝑤 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝑤 } ∈ 𝐸 ) )
89 df-reu ⊢ ( ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 ↔ ∃! 𝑤 ( 𝑤 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝑤 } ∈ 𝐸 ) )
90 88 89 sylibr ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 )
91 90 ex ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐴 , 𝐵 } ∈ 𝐸 → ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 ) )