Metamath Proof Explorer


Theorem imasleval

Description: The value of the image structure's ordering when the order is compatible with the mapping function. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses imasless.u ( 𝜑𝑈 = ( 𝐹s 𝑅 ) )
imasless.v ( 𝜑𝑉 = ( Base ‘ 𝑅 ) )
imasless.f ( 𝜑𝐹 : 𝑉onto𝐵 )
imasless.r ( 𝜑𝑅𝑍 )
imasless.l = ( le ‘ 𝑈 )
imasleval.n 𝑁 = ( le ‘ 𝑅 )
imasleval.e ( ( 𝜑 ∧ ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑐𝑉𝑑𝑉 ) ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ∧ ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ) → ( 𝑎 𝑁 𝑏𝑐 𝑁 𝑑 ) ) )
Assertion imasleval ( ( 𝜑𝑋𝑉𝑌𝑉 ) → ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ↔ 𝑋 𝑁 𝑌 ) )

Proof

Step Hyp Ref Expression
1 imasless.u ( 𝜑𝑈 = ( 𝐹s 𝑅 ) )
2 imasless.v ( 𝜑𝑉 = ( Base ‘ 𝑅 ) )
3 imasless.f ( 𝜑𝐹 : 𝑉onto𝐵 )
4 imasless.r ( 𝜑𝑅𝑍 )
5 imasless.l = ( le ‘ 𝑈 )
6 imasleval.n 𝑁 = ( le ‘ 𝑅 )
7 imasleval.e ( ( 𝜑 ∧ ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑐𝑉𝑑𝑉 ) ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ∧ ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ) → ( 𝑎 𝑁 𝑏𝑐 𝑁 𝑑 ) ) )
8 fveq2 ( 𝑐 = 𝑋 → ( 𝐹𝑐 ) = ( 𝐹𝑋 ) )
9 8 breq1d ( 𝑐 = 𝑋 → ( ( 𝐹𝑐 ) ( 𝐹𝑑 ) ↔ ( 𝐹𝑋 ) ( 𝐹𝑑 ) ) )
10 breq1 ( 𝑐 = 𝑋 → ( 𝑐 𝑁 𝑑𝑋 𝑁 𝑑 ) )
11 9 10 bibi12d ( 𝑐 = 𝑋 → ( ( ( 𝐹𝑐 ) ( 𝐹𝑑 ) ↔ 𝑐 𝑁 𝑑 ) ↔ ( ( 𝐹𝑋 ) ( 𝐹𝑑 ) ↔ 𝑋 𝑁 𝑑 ) ) )
12 11 imbi2d ( 𝑐 = 𝑋 → ( ( 𝜑 → ( ( 𝐹𝑐 ) ( 𝐹𝑑 ) ↔ 𝑐 𝑁 𝑑 ) ) ↔ ( 𝜑 → ( ( 𝐹𝑋 ) ( 𝐹𝑑 ) ↔ 𝑋 𝑁 𝑑 ) ) ) )
13 fveq2 ( 𝑑 = 𝑌 → ( 𝐹𝑑 ) = ( 𝐹𝑌 ) )
14 13 breq2d ( 𝑑 = 𝑌 → ( ( 𝐹𝑋 ) ( 𝐹𝑑 ) ↔ ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) )
15 breq2 ( 𝑑 = 𝑌 → ( 𝑋 𝑁 𝑑𝑋 𝑁 𝑌 ) )
16 14 15 bibi12d ( 𝑑 = 𝑌 → ( ( ( 𝐹𝑋 ) ( 𝐹𝑑 ) ↔ 𝑋 𝑁 𝑑 ) ↔ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ↔ 𝑋 𝑁 𝑌 ) ) )
17 16 imbi2d ( 𝑑 = 𝑌 → ( ( 𝜑 → ( ( 𝐹𝑋 ) ( 𝐹𝑑 ) ↔ 𝑋 𝑁 𝑑 ) ) ↔ ( 𝜑 → ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ↔ 𝑋 𝑁 𝑌 ) ) ) )
18 fofn ( 𝐹 : 𝑉onto𝐵𝐹 Fn 𝑉 )
19 3 18 syl ( 𝜑𝐹 Fn 𝑉 )
20 19 adantr ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) → 𝐹 Fn 𝑉 )
21 20 fndmd ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) → dom 𝐹 = 𝑉 )
22 21 rexeqdv ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) → ( ∃ 𝑎 ∈ dom 𝐹 ( 𝑎 𝐹 ( 𝐹𝑐 ) ∧ 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) ↔ ∃ 𝑎𝑉 ( 𝑎 𝐹 ( 𝐹𝑐 ) ∧ 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) ) )
23 fnbrfvb ( ( 𝐹 Fn 𝑉𝑎𝑉 ) → ( ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ↔ 𝑎 𝐹 ( 𝐹𝑐 ) ) )
24 20 23 sylan ( ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) ∧ 𝑎𝑉 ) → ( ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ↔ 𝑎 𝐹 ( 𝐹𝑐 ) ) )
25 24 anbi1d ( ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) ∧ 𝑎𝑉 ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ∧ 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) ↔ ( 𝑎 𝐹 ( 𝐹𝑐 ) ∧ 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) ) )
26 ancom ( ( 𝑎 𝑁 𝑏𝑏 𝐹 ( 𝐹𝑑 ) ) ↔ ( 𝑏 𝐹 ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) )
27 vex 𝑏 ∈ V
28 fvex ( 𝐹𝑑 ) ∈ V
29 27 28 breldm ( 𝑏 𝐹 ( 𝐹𝑑 ) → 𝑏 ∈ dom 𝐹 )
30 29 adantr ( ( 𝑏 𝐹 ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) → 𝑏 ∈ dom 𝐹 )
31 30 pm4.71ri ( ( 𝑏 𝐹 ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) ↔ ( 𝑏 ∈ dom 𝐹 ∧ ( 𝑏 𝐹 ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) ) )
32 26 31 bitri ( ( 𝑎 𝑁 𝑏𝑏 𝐹 ( 𝐹𝑑 ) ) ↔ ( 𝑏 ∈ dom 𝐹 ∧ ( 𝑏 𝐹 ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) ) )
33 32 exbii ( ∃ 𝑏 ( 𝑎 𝑁 𝑏𝑏 𝐹 ( 𝐹𝑑 ) ) ↔ ∃ 𝑏 ( 𝑏 ∈ dom 𝐹 ∧ ( 𝑏 𝐹 ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) ) )
34 vex 𝑎 ∈ V
35 34 28 brco ( 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ↔ ∃ 𝑏 ( 𝑎 𝑁 𝑏𝑏 𝐹 ( 𝐹𝑑 ) ) )
36 df-rex ( ∃ 𝑏 ∈ dom 𝐹 ( 𝑏 𝐹 ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) ↔ ∃ 𝑏 ( 𝑏 ∈ dom 𝐹 ∧ ( 𝑏 𝐹 ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) ) )
37 33 35 36 3bitr4i ( 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ↔ ∃ 𝑏 ∈ dom 𝐹 ( 𝑏 𝐹 ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) )
38 20 ad2antrr ( ( ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) ∧ 𝑎𝑉 ) ∧ ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ) → 𝐹 Fn 𝑉 )
39 fnbrfvb ( ( 𝐹 Fn 𝑉𝑏𝑉 ) → ( ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ↔ 𝑏 𝐹 ( 𝐹𝑑 ) ) )
40 38 39 sylan ( ( ( ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) ∧ 𝑎𝑉 ) ∧ ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ) ∧ 𝑏𝑉 ) → ( ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ↔ 𝑏 𝐹 ( 𝐹𝑑 ) ) )
41 40 anbi1d ( ( ( ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) ∧ 𝑎𝑉 ) ∧ ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ) ∧ 𝑏𝑉 ) → ( ( ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) ↔ ( 𝑏 𝐹 ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) ) )
42 7 3expa ( ( ( 𝜑 ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ ( 𝑐𝑉𝑑𝑉 ) ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ∧ ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ) → ( 𝑎 𝑁 𝑏𝑐 𝑁 𝑑 ) ) )
43 42 an32s ( ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ∧ ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ) → ( 𝑎 𝑁 𝑏𝑐 𝑁 𝑑 ) ) )
44 43 anassrs ( ( ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) ∧ 𝑎𝑉 ) ∧ 𝑏𝑉 ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ∧ ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ) → ( 𝑎 𝑁 𝑏𝑐 𝑁 𝑑 ) ) )
45 44 impl ( ( ( ( ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) ∧ 𝑎𝑉 ) ∧ 𝑏𝑉 ) ∧ ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ) ∧ ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ) → ( 𝑎 𝑁 𝑏𝑐 𝑁 𝑑 ) )
46 45 pm5.32da ( ( ( ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) ∧ 𝑎𝑉 ) ∧ 𝑏𝑉 ) ∧ ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ) → ( ( ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) ↔ ( ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ∧ 𝑐 𝑁 𝑑 ) ) )
47 46 an32s ( ( ( ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) ∧ 𝑎𝑉 ) ∧ ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ) ∧ 𝑏𝑉 ) → ( ( ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) ↔ ( ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ∧ 𝑐 𝑁 𝑑 ) ) )
48 41 47 bitr3d ( ( ( ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) ∧ 𝑎𝑉 ) ∧ ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ) ∧ 𝑏𝑉 ) → ( ( 𝑏 𝐹 ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) ↔ ( ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ∧ 𝑐 𝑁 𝑑 ) ) )
49 48 rexbidva ( ( ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) ∧ 𝑎𝑉 ) ∧ ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ) → ( ∃ 𝑏𝑉 ( 𝑏 𝐹 ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) ↔ ∃ 𝑏𝑉 ( ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ∧ 𝑐 𝑁 𝑑 ) ) )
50 r19.41v ( ∃ 𝑏𝑉 ( ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ∧ 𝑐 𝑁 𝑑 ) ↔ ( ∃ 𝑏𝑉 ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ∧ 𝑐 𝑁 𝑑 ) )
51 49 50 bitrdi ( ( ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) ∧ 𝑎𝑉 ) ∧ ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ) → ( ∃ 𝑏𝑉 ( 𝑏 𝐹 ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) ↔ ( ∃ 𝑏𝑉 ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ∧ 𝑐 𝑁 𝑑 ) ) )
52 21 rexeqdv ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) → ( ∃ 𝑏 ∈ dom 𝐹 ( 𝑏 𝐹 ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) ↔ ∃ 𝑏𝑉 ( 𝑏 𝐹 ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) ) )
53 52 ad2antrr ( ( ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) ∧ 𝑎𝑉 ) ∧ ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ) → ( ∃ 𝑏 ∈ dom 𝐹 ( 𝑏 𝐹 ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) ↔ ∃ 𝑏𝑉 ( 𝑏 𝐹 ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) ) )
54 simprr ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) → 𝑑𝑉 )
55 eqid ( 𝐹𝑑 ) = ( 𝐹𝑑 )
56 fveqeq2 ( 𝑏 = 𝑑 → ( ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ↔ ( 𝐹𝑑 ) = ( 𝐹𝑑 ) ) )
57 56 rspcev ( ( 𝑑𝑉 ∧ ( 𝐹𝑑 ) = ( 𝐹𝑑 ) ) → ∃ 𝑏𝑉 ( 𝐹𝑏 ) = ( 𝐹𝑑 ) )
58 54 55 57 sylancl ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) → ∃ 𝑏𝑉 ( 𝐹𝑏 ) = ( 𝐹𝑑 ) )
59 58 biantrurd ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) → ( 𝑐 𝑁 𝑑 ↔ ( ∃ 𝑏𝑉 ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ∧ 𝑐 𝑁 𝑑 ) ) )
60 59 ad2antrr ( ( ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) ∧ 𝑎𝑉 ) ∧ ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ) → ( 𝑐 𝑁 𝑑 ↔ ( ∃ 𝑏𝑉 ( 𝐹𝑏 ) = ( 𝐹𝑑 ) ∧ 𝑐 𝑁 𝑑 ) ) )
61 51 53 60 3bitr4d ( ( ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) ∧ 𝑎𝑉 ) ∧ ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ) → ( ∃ 𝑏 ∈ dom 𝐹 ( 𝑏 𝐹 ( 𝐹𝑑 ) ∧ 𝑎 𝑁 𝑏 ) ↔ 𝑐 𝑁 𝑑 ) )
62 37 61 syl5bb ( ( ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) ∧ 𝑎𝑉 ) ∧ ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ) → ( 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ↔ 𝑐 𝑁 𝑑 ) )
63 62 pm5.32da ( ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) ∧ 𝑎𝑉 ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ∧ 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) ↔ ( ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ∧ 𝑐 𝑁 𝑑 ) ) )
64 25 63 bitr3d ( ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) ∧ 𝑎𝑉 ) → ( ( 𝑎 𝐹 ( 𝐹𝑐 ) ∧ 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) ↔ ( ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ∧ 𝑐 𝑁 𝑑 ) ) )
65 64 rexbidva ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) → ( ∃ 𝑎𝑉 ( 𝑎 𝐹 ( 𝐹𝑐 ) ∧ 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) ↔ ∃ 𝑎𝑉 ( ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ∧ 𝑐 𝑁 𝑑 ) ) )
66 22 65 bitrd ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) → ( ∃ 𝑎 ∈ dom 𝐹 ( 𝑎 𝐹 ( 𝐹𝑐 ) ∧ 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) ↔ ∃ 𝑎𝑉 ( ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ∧ 𝑐 𝑁 𝑑 ) ) )
67 fvex ( 𝐹𝑐 ) ∈ V
68 67 34 brcnv ( ( 𝐹𝑐 ) 𝐹 𝑎𝑎 𝐹 ( 𝐹𝑐 ) )
69 68 anbi1i ( ( ( 𝐹𝑐 ) 𝐹 𝑎𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) ↔ ( 𝑎 𝐹 ( 𝐹𝑐 ) ∧ 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) )
70 34 67 breldm ( 𝑎 𝐹 ( 𝐹𝑐 ) → 𝑎 ∈ dom 𝐹 )
71 70 adantr ( ( 𝑎 𝐹 ( 𝐹𝑐 ) ∧ 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) → 𝑎 ∈ dom 𝐹 )
72 71 pm4.71ri ( ( 𝑎 𝐹 ( 𝐹𝑐 ) ∧ 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) ↔ ( 𝑎 ∈ dom 𝐹 ∧ ( 𝑎 𝐹 ( 𝐹𝑐 ) ∧ 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) ) )
73 69 72 bitri ( ( ( 𝐹𝑐 ) 𝐹 𝑎𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) ↔ ( 𝑎 ∈ dom 𝐹 ∧ ( 𝑎 𝐹 ( 𝐹𝑐 ) ∧ 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) ) )
74 73 exbii ( ∃ 𝑎 ( ( 𝐹𝑐 ) 𝐹 𝑎𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) ↔ ∃ 𝑎 ( 𝑎 ∈ dom 𝐹 ∧ ( 𝑎 𝐹 ( 𝐹𝑐 ) ∧ 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) ) )
75 67 28 brco ( ( 𝐹𝑐 ) ( ( 𝐹𝑁 ) ∘ 𝐹 ) ( 𝐹𝑑 ) ↔ ∃ 𝑎 ( ( 𝐹𝑐 ) 𝐹 𝑎𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) )
76 df-rex ( ∃ 𝑎 ∈ dom 𝐹 ( 𝑎 𝐹 ( 𝐹𝑐 ) ∧ 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) ↔ ∃ 𝑎 ( 𝑎 ∈ dom 𝐹 ∧ ( 𝑎 𝐹 ( 𝐹𝑐 ) ∧ 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) ) )
77 74 75 76 3bitr4ri ( ∃ 𝑎 ∈ dom 𝐹 ( 𝑎 𝐹 ( 𝐹𝑐 ) ∧ 𝑎 ( 𝐹𝑁 ) ( 𝐹𝑑 ) ) ↔ ( 𝐹𝑐 ) ( ( 𝐹𝑁 ) ∘ 𝐹 ) ( 𝐹𝑑 ) )
78 r19.41v ( ∃ 𝑎𝑉 ( ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ∧ 𝑐 𝑁 𝑑 ) ↔ ( ∃ 𝑎𝑉 ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ∧ 𝑐 𝑁 𝑑 ) )
79 66 77 78 3bitr3g ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) → ( ( 𝐹𝑐 ) ( ( 𝐹𝑁 ) ∘ 𝐹 ) ( 𝐹𝑑 ) ↔ ( ∃ 𝑎𝑉 ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ∧ 𝑐 𝑁 𝑑 ) ) )
80 1 2 3 4 6 5 imasle ( 𝜑 = ( ( 𝐹𝑁 ) ∘ 𝐹 ) )
81 80 adantr ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) → = ( ( 𝐹𝑁 ) ∘ 𝐹 ) )
82 81 breqd ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) → ( ( 𝐹𝑐 ) ( 𝐹𝑑 ) ↔ ( 𝐹𝑐 ) ( ( 𝐹𝑁 ) ∘ 𝐹 ) ( 𝐹𝑑 ) ) )
83 simprl ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) → 𝑐𝑉 )
84 eqid ( 𝐹𝑐 ) = ( 𝐹𝑐 )
85 fveqeq2 ( 𝑎 = 𝑐 → ( ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ↔ ( 𝐹𝑐 ) = ( 𝐹𝑐 ) ) )
86 85 rspcev ( ( 𝑐𝑉 ∧ ( 𝐹𝑐 ) = ( 𝐹𝑐 ) ) → ∃ 𝑎𝑉 ( 𝐹𝑎 ) = ( 𝐹𝑐 ) )
87 83 84 86 sylancl ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) → ∃ 𝑎𝑉 ( 𝐹𝑎 ) = ( 𝐹𝑐 ) )
88 87 biantrurd ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) → ( 𝑐 𝑁 𝑑 ↔ ( ∃ 𝑎𝑉 ( 𝐹𝑎 ) = ( 𝐹𝑐 ) ∧ 𝑐 𝑁 𝑑 ) ) )
89 79 82 88 3bitr4d ( ( 𝜑 ∧ ( 𝑐𝑉𝑑𝑉 ) ) → ( ( 𝐹𝑐 ) ( 𝐹𝑑 ) ↔ 𝑐 𝑁 𝑑 ) )
90 89 expcom ( ( 𝑐𝑉𝑑𝑉 ) → ( 𝜑 → ( ( 𝐹𝑐 ) ( 𝐹𝑑 ) ↔ 𝑐 𝑁 𝑑 ) ) )
91 12 17 90 vtocl2ga ( ( 𝑋𝑉𝑌𝑉 ) → ( 𝜑 → ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ↔ 𝑋 𝑁 𝑌 ) ) )
92 91 com12 ( 𝜑 → ( ( 𝑋𝑉𝑌𝑉 ) → ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ↔ 𝑋 𝑁 𝑌 ) ) )
93 92 3impib ( ( 𝜑𝑋𝑉𝑌𝑉 ) → ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ↔ 𝑋 𝑁 𝑌 ) )