Metamath Proof Explorer

Theorem isubgr3stgrlem4

Description: Lemma 4 for isubgr3stgr . (Contributed by AV, 24-Sep-2025)

Ref Expression
Hypotheses isubgr3stgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isubgr3stgr.u ⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
isubgr3stgr.c ⊢ 𝐶 = ( 𝐺 ClNeighbVtx 𝑋 )
isubgr3stgr.n ⊢ 𝑁 ∈ ℕ0
isubgr3stgr.s ⊢ 𝑆 = ( StarGr ‘ 𝑁 )
isubgr3stgr.w ⊢ 𝑊 = ( Vtx ‘ 𝑆 )
isubgr3stgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion isubgr3stgrlem4 ( ( 𝐴 = 𝑋 ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ∃ 𝑧 ∈ ( 1 ... 𝑁 ) ( 𝐹 “ { 𝐴 , 𝐵 } ) = { 0 , 𝑧 } )

Proof

Step Hyp Ref Expression
1 isubgr3stgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isubgr3stgr.u ⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
3 isubgr3stgr.c ⊢ 𝐶 = ( 𝐺 ClNeighbVtx 𝑋 )
4 isubgr3stgr.n ⊢ 𝑁 ∈ ℕ0
5 isubgr3stgr.s ⊢ 𝑆 = ( StarGr ‘ 𝑁 )
6 isubgr3stgr.w ⊢ 𝑊 = ( Vtx ‘ 𝑆 )
7 isubgr3stgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
8 preq2 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝐵 ) → { 0 , 𝑧 } = { 0 , ( 𝐹 ‘ 𝐵 ) } )
9 8 eqeq2d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝐵 ) → ( ( 𝐹 “ { 𝑋 , 𝐵 } ) = { 0 , 𝑧 } ↔ ( 𝐹 “ { 𝑋 , 𝐵 } ) = { 0 , ( 𝐹 ‘ 𝐵 ) } ) )
10 f1of ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 → 𝐹 : 𝐶 ⟶ 𝑊 )
11 10 adantr ⊢ ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) → 𝐹 : 𝐶 ⟶ 𝑊 )
12 11 adantr ⊢ ( ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → 𝐹 : 𝐶 ⟶ 𝑊 )
13 simpr3 ⊢ ( ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → 𝐵 ∈ 𝐶 )
14 12 13 ffvelcdmd ⊢ ( ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ 𝑊 )
15 5 fveq2i ⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ ( StarGr ‘ 𝑁 ) )
16 stgrvtx ⊢ ( 𝑁 ∈ ℕ0 → ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) = ( 0 ... 𝑁 ) )
17 4 16 ax-mp ⊢ ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) = ( 0 ... 𝑁 )
18 6 15 17 3eqtri ⊢ 𝑊 = ( 0 ... 𝑁 )
19 18 eleq2i ⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ 𝑊 ↔ ( 𝐹 ‘ 𝐵 ) ∈ ( 0 ... 𝑁 ) )
20 fz0sn0fz1 ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ... 𝑁 ) = ( { 0 } ∪ ( 1 ... 𝑁 ) ) )
21 4 20 ax-mp ⊢ ( 0 ... 𝑁 ) = ( { 0 } ∪ ( 1 ... 𝑁 ) )
22 21 eleq2i ⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ( 0 ... 𝑁 ) ↔ ( 𝐹 ‘ 𝐵 ) ∈ ( { 0 } ∪ ( 1 ... 𝑁 ) ) )
23 elun ⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ( { 0 } ∪ ( 1 ... 𝑁 ) ) ↔ ( ( 𝐹 ‘ 𝐵 ) ∈ { 0 } ∨ ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
24 fvex ⊢ ( 𝐹 ‘ 𝐵 ) ∈ V
25 24 elsn ⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ { 0 } ↔ ( 𝐹 ‘ 𝐵 ) = 0 )
26 25 orbi1i ⊢ ( ( ( 𝐹 ‘ 𝐵 ) ∈ { 0 } ∨ ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) ↔ ( ( 𝐹 ‘ 𝐵 ) = 0 ∨ ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
27 23 26 bitri ⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ( { 0 } ∪ ( 1 ... 𝑁 ) ) ↔ ( ( 𝐹 ‘ 𝐵 ) = 0 ∨ ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
28 19 22 27 3bitri ⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ 𝑊 ↔ ( ( 𝐹 ‘ 𝐵 ) = 0 ∨ ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
29 eqeq2 ⊢ ( ( 𝐹 ‘ 𝑋 ) = 0 → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝐵 ) = 0 ) )
30 29 adantl ⊢ ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝐵 ) = 0 ) )
31 30 adantr ⊢ ( ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝐵 ) = 0 ) )
32 f1of1 ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 → 𝐹 : 𝐶 –1-1→ 𝑊 )
33 dff14a ⊢ ( 𝐹 : 𝐶 –1-1→ 𝑊 ↔ ( 𝐹 : 𝐶 ⟶ 𝑊 ∧ ∀ 𝑎 ∈ 𝐶 ∀ 𝑏 ∈ 𝐶 ( 𝑎 ≠ 𝑏 → ( 𝐹 ‘ 𝑎 ) ≠ ( 𝐹 ‘ 𝑏 ) ) ) )
34 simpl ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝐵 ) → 𝑎 = 𝑋 )
35 simpr ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
36 34 35 neeq12d ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝐵 ) → ( 𝑎 ≠ 𝑏 ↔ 𝑋 ≠ 𝐵 ) )
37 fveq2 ⊢ ( 𝑎 = 𝑋 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑋 ) )
38 37 adantr ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝐵 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑋 ) )
39 fveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝐵 ) )
40 39 adantl ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝐵 ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝐵 ) )
41 38 40 neeq12d ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝐵 ) → ( ( 𝐹 ‘ 𝑎 ) ≠ ( 𝐹 ‘ 𝑏 ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝐵 ) ) )
42 36 41 imbi12d ⊢ ( ( 𝑎 = 𝑋 ∧ 𝑏 = 𝐵 ) → ( ( 𝑎 ≠ 𝑏 → ( 𝐹 ‘ 𝑎 ) ≠ ( 𝐹 ‘ 𝑏 ) ) ↔ ( 𝑋 ≠ 𝐵 → ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝐵 ) ) ) )
43 42 rspc2gv ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( ∀ 𝑎 ∈ 𝐶 ∀ 𝑏 ∈ 𝐶 ( 𝑎 ≠ 𝑏 → ( 𝐹 ‘ 𝑎 ) ≠ ( 𝐹 ‘ 𝑏 ) ) → ( 𝑋 ≠ 𝐵 → ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝐵 ) ) ) )
44 43 3adant1 ⊢ ( ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( ∀ 𝑎 ∈ 𝐶 ∀ 𝑏 ∈ 𝐶 ( 𝑎 ≠ 𝑏 → ( 𝐹 ‘ 𝑎 ) ≠ ( 𝐹 ‘ 𝑏 ) ) → ( 𝑋 ≠ 𝐵 → ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝐵 ) ) ) )
45 id ⊢ ( ( 𝑋 ≠ 𝐵 → ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝐵 ) ) → ( 𝑋 ≠ 𝐵 → ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝐵 ) ) )
46 eqneqall ⊢ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝐵 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
47 46 eqcoms ⊢ ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝑋 ) → ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝐵 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
48 47 com12 ⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝐵 ) → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝑋 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
49 45 48 syl6com ⊢ ( 𝑋 ≠ 𝐵 → ( ( 𝑋 ≠ 𝐵 → ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝐵 ) ) → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝑋 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) ) )
50 49 3ad2ant1 ⊢ ( ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝑋 ≠ 𝐵 → ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝐵 ) ) → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝑋 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) ) )
51 44 50 syld ⊢ ( ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( ∀ 𝑎 ∈ 𝐶 ∀ 𝑏 ∈ 𝐶 ( 𝑎 ≠ 𝑏 → ( 𝐹 ‘ 𝑎 ) ≠ ( 𝐹 ‘ 𝑏 ) ) → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝑋 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) ) )
52 51 adantld ⊢ ( ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝐹 : 𝐶 ⟶ 𝑊 ∧ ∀ 𝑎 ∈ 𝐶 ∀ 𝑏 ∈ 𝐶 ( 𝑎 ≠ 𝑏 → ( 𝐹 ‘ 𝑎 ) ≠ ( 𝐹 ‘ 𝑏 ) ) ) → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝑋 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) ) )
53 33 52 biimtrid ⊢ ( ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐹 : 𝐶 –1-1→ 𝑊 → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝑋 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) ) )
54 32 53 syl5com ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 → ( ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝑋 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) ) )
55 54 adantr ⊢ ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) → ( ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝑋 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) ) )
56 55 imp ⊢ ( ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝑋 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
57 31 56 sylbird ⊢ ( ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝐵 ) = 0 → ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
58 idd ⊢ ( ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
59 57 58 jaod ⊢ ( ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( ( ( 𝐹 ‘ 𝐵 ) = 0 ∨ ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
60 28 59 biimtrid ⊢ ( ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝐵 ) ∈ 𝑊 → ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) ) )
61 14 60 mpd ⊢ ( ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 1 ... 𝑁 ) )
62 f1ofn ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 → 𝐹 Fn 𝐶 )
63 62 adantr ⊢ ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) → 𝐹 Fn 𝐶 )
64 3simpc ⊢ ( ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) )
65 63 64 anim12i ⊢ ( ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( 𝐹 Fn 𝐶 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) )
66 3anass ⊢ ( ( 𝐹 Fn 𝐶 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ↔ ( 𝐹 Fn 𝐶 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) )
67 65 66 sylibr ⊢ ( ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( 𝐹 Fn 𝐶 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) )
68 fnimapr ⊢ ( ( 𝐹 Fn 𝐶 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐹 “ { 𝑋 , 𝐵 } ) = { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝐵 ) } )
69 67 68 syl ⊢ ( ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( 𝐹 “ { 𝑋 , 𝐵 } ) = { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝐵 ) } )
70 simpr ⊢ ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) → ( 𝐹 ‘ 𝑋 ) = 0 )
71 70 adantr ⊢ ( ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑋 ) = 0 )
72 71 preq1d ⊢ ( ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝐵 ) } = { 0 , ( 𝐹 ‘ 𝐵 ) } )
73 69 72 eqtrd ⊢ ( ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ( 𝐹 “ { 𝑋 , 𝐵 } ) = { 0 , ( 𝐹 ‘ 𝐵 ) } )
74 9 61 73 rspcedvdw ⊢ ( ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ∃ 𝑧 ∈ ( 1 ... 𝑁 ) ( 𝐹 “ { 𝑋 , 𝐵 } ) = { 0 , 𝑧 } )
75 74 ex ⊢ ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) → ( ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ∃ 𝑧 ∈ ( 1 ... 𝑁 ) ( 𝐹 “ { 𝑋 , 𝐵 } ) = { 0 , 𝑧 } ) )
76 neeq1 ⊢ ( 𝐴 = 𝑋 → ( 𝐴 ≠ 𝐵 ↔ 𝑋 ≠ 𝐵 ) )
77 eleq1 ⊢ ( 𝐴 = 𝑋 → ( 𝐴 ∈ 𝐶 ↔ 𝑋 ∈ 𝐶 ) )
78 76 77 3anbi12d ⊢ ( 𝐴 = 𝑋 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ↔ ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) )
79 preq1 ⊢ ( 𝐴 = 𝑋 → { 𝐴 , 𝐵 } = { 𝑋 , 𝐵 } )
80 79 imaeq2d ⊢ ( 𝐴 = 𝑋 → ( 𝐹 “ { 𝐴 , 𝐵 } ) = ( 𝐹 “ { 𝑋 , 𝐵 } ) )
81 80 eqeq1d ⊢ ( 𝐴 = 𝑋 → ( ( 𝐹 “ { 𝐴 , 𝐵 } ) = { 0 , 𝑧 } ↔ ( 𝐹 “ { 𝑋 , 𝐵 } ) = { 0 , 𝑧 } ) )
82 81 rexbidv ⊢ ( 𝐴 = 𝑋 → ( ∃ 𝑧 ∈ ( 1 ... 𝑁 ) ( 𝐹 “ { 𝐴 , 𝐵 } ) = { 0 , 𝑧 } ↔ ∃ 𝑧 ∈ ( 1 ... 𝑁 ) ( 𝐹 “ { 𝑋 , 𝐵 } ) = { 0 , 𝑧 } ) )
83 78 82 imbi12d ⊢ ( 𝐴 = 𝑋 → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ∃ 𝑧 ∈ ( 1 ... 𝑁 ) ( 𝐹 “ { 𝐴 , 𝐵 } ) = { 0 , 𝑧 } ) ↔ ( ( 𝑋 ≠ 𝐵 ∧ 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ∃ 𝑧 ∈ ( 1 ... 𝑁 ) ( 𝐹 “ { 𝑋 , 𝐵 } ) = { 0 , 𝑧 } ) ) )
84 75 83 imbitrrid ⊢ ( 𝐴 = 𝑋 → ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ∃ 𝑧 ∈ ( 1 ... 𝑁 ) ( 𝐹 “ { 𝐴 , 𝐵 } ) = { 0 , 𝑧 } ) ) )
85 84 3imp ⊢ ( ( 𝐴 = 𝑋 ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ) → ∃ 𝑧 ∈ ( 1 ... 𝑁 ) ( 𝐹 “ { 𝐴 , 𝐵 } ) = { 0 , 𝑧 } )