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 bitrid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑐 ) ) → ( 𝑎 ( 𝐹 ∘ 𝑁 ) ( 𝐹 ‘ 𝑑 ) ↔ 𝑐 𝑁 𝑑 ) )
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 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑋 ) ≤ ( 𝐹 ‘ 𝑌 ) ↔ 𝑋 𝑁 𝑌 ) )