Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  imasleval Structured version   Visualization version   GIF version

Theorem imasleval 16122
 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.)
Hypotheses
Ref Expression
imasless.u (𝜑𝑈 = (𝐹s 𝑅))
imasless.v (𝜑𝑉 = (Base‘𝑅))
imasless.f (𝜑𝐹:𝑉onto𝐵)
imasless.r (𝜑𝑅𝑍)
imasless.l = (le‘𝑈)
imasleval.n 𝑁 = (le‘𝑅)
imasleval.e ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑐𝑉𝑑𝑉)) → (((𝐹𝑎) = (𝐹𝑐) ∧ (𝐹𝑏) = (𝐹𝑑)) → (𝑎𝑁𝑏𝑐𝑁𝑑)))
Assertion
Ref Expression
imasleval ((𝜑𝑋𝑉𝑌𝑉) → ((𝐹𝑋) (𝐹𝑌) ↔ 𝑋𝑁𝑌))
Distinct variable groups:   𝑐,𝑑,   𝑎,𝑏,𝑐,𝑑,𝐹   𝑁,𝑎,𝑏,𝑐,𝑑   𝑉,𝑎,𝑏,𝑐,𝑑   𝑌,𝑑   𝜑,𝑎,𝑏,𝑐,𝑑   𝑋,𝑐,𝑑
Allowed substitution hints:   𝐵(𝑎,𝑏,𝑐,𝑑)   𝑅(𝑎,𝑏,𝑐,𝑑)   𝑈(𝑎,𝑏,𝑐,𝑑)   (𝑎,𝑏)   𝑋(𝑎,𝑏)   𝑌(𝑎,𝑏,𝑐)   𝑍(𝑎,𝑏,𝑐,𝑑)

Proof of Theorem imasleval
StepHypRef Expression
1 fveq2 6148 . . . . . . 7 (𝑐 = 𝑋 → (𝐹𝑐) = (𝐹𝑋))
21breq1d 4623 . . . . . 6 (𝑐 = 𝑋 → ((𝐹𝑐) (𝐹𝑑) ↔ (𝐹𝑋) (𝐹𝑑)))
3 breq1 4616 . . . . . 6 (𝑐 = 𝑋 → (𝑐𝑁𝑑𝑋𝑁𝑑))
42, 3bibi12d 335 . . . . 5 (𝑐 = 𝑋 → (((𝐹𝑐) (𝐹𝑑) ↔ 𝑐𝑁𝑑) ↔ ((𝐹𝑋) (𝐹𝑑) ↔ 𝑋𝑁𝑑)))
54imbi2d 330 . . . 4 (𝑐 = 𝑋 → ((𝜑 → ((𝐹𝑐) (𝐹𝑑) ↔ 𝑐𝑁𝑑)) ↔ (𝜑 → ((𝐹𝑋) (𝐹𝑑) ↔ 𝑋𝑁𝑑))))
6 fveq2 6148 . . . . . . 7 (𝑑 = 𝑌 → (𝐹𝑑) = (𝐹𝑌))
76breq2d 4625 . . . . . 6 (𝑑 = 𝑌 → ((𝐹𝑋) (𝐹𝑑) ↔ (𝐹𝑋) (𝐹𝑌)))
8 breq2 4617 . . . . . 6 (𝑑 = 𝑌 → (𝑋𝑁𝑑𝑋𝑁𝑌))
97, 8bibi12d 335 . . . . 5 (𝑑 = 𝑌 → (((𝐹𝑋) (𝐹𝑑) ↔ 𝑋𝑁𝑑) ↔ ((𝐹𝑋) (𝐹𝑌) ↔ 𝑋𝑁𝑌)))
109imbi2d 330 . . . 4 (𝑑 = 𝑌 → ((𝜑 → ((𝐹𝑋) (𝐹𝑑) ↔ 𝑋𝑁𝑑)) ↔ (𝜑 → ((𝐹𝑋) (𝐹𝑌) ↔ 𝑋𝑁𝑌))))
11 imasless.f . . . . . . . . . . . 12 (𝜑𝐹:𝑉onto𝐵)
12 fofn 6074 . . . . . . . . . . . 12 (𝐹:𝑉onto𝐵𝐹 Fn 𝑉)
1311, 12syl 17 . . . . . . . . . . 11 (𝜑𝐹 Fn 𝑉)
1413adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑐𝑉𝑑𝑉)) → 𝐹 Fn 𝑉)
15 fndm 5948 . . . . . . . . . 10 (𝐹 Fn 𝑉 → dom 𝐹 = 𝑉)
1614, 15syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑐𝑉𝑑𝑉)) → dom 𝐹 = 𝑉)
1716rexeqdv 3134 . . . . . . . 8 ((𝜑 ∧ (𝑐𝑉𝑑𝑉)) → (∃𝑎 ∈ dom 𝐹(𝑎𝐹(𝐹𝑐) ∧ 𝑎(𝐹𝑁)(𝐹𝑑)) ↔ ∃𝑎𝑉 (𝑎𝐹(𝐹𝑐) ∧ 𝑎(𝐹𝑁)(𝐹𝑑))))
18 fnbrfvb 6193 . . . . . . . . . . . 12 ((𝐹 Fn 𝑉𝑎𝑉) → ((𝐹𝑎) = (𝐹𝑐) ↔ 𝑎𝐹(𝐹𝑐)))
1914, 18sylan 488 . . . . . . . . . . 11 (((𝜑 ∧ (𝑐𝑉𝑑𝑉)) ∧ 𝑎𝑉) → ((𝐹𝑎) = (𝐹𝑐) ↔ 𝑎𝐹(𝐹𝑐)))
2019anbi1d 740 . . . . . . . . . 10 (((𝜑 ∧ (𝑐𝑉𝑑𝑉)) ∧ 𝑎𝑉) → (((𝐹𝑎) = (𝐹𝑐) ∧ 𝑎(𝐹𝑁)(𝐹𝑑)) ↔ (𝑎𝐹(𝐹𝑐) ∧ 𝑎(𝐹𝑁)(𝐹𝑑))))
21 ancom 466 . . . . . . . . . . . . . . 15 ((𝑎𝑁𝑏𝑏𝐹(𝐹𝑑)) ↔ (𝑏𝐹(𝐹𝑑) ∧ 𝑎𝑁𝑏))
22 vex 3189 . . . . . . . . . . . . . . . . . 18 𝑏 ∈ V
23 fvex 6158 . . . . . . . . . . . . . . . . . 18 (𝐹𝑑) ∈ V
2422, 23breldm 5289 . . . . . . . . . . . . . . . . 17 (𝑏𝐹(𝐹𝑑) → 𝑏 ∈ dom 𝐹)
2524adantr 481 . . . . . . . . . . . . . . . 16 ((𝑏𝐹(𝐹𝑑) ∧ 𝑎𝑁𝑏) → 𝑏 ∈ dom 𝐹)
2625pm4.71ri 664 . . . . . . . . . . . . . . 15 ((𝑏𝐹(𝐹𝑑) ∧ 𝑎𝑁𝑏) ↔ (𝑏 ∈ dom 𝐹 ∧ (𝑏𝐹(𝐹𝑑) ∧ 𝑎𝑁𝑏)))
2721, 26bitri 264 . . . . . . . . . . . . . 14 ((𝑎𝑁𝑏𝑏𝐹(𝐹𝑑)) ↔ (𝑏 ∈ dom 𝐹 ∧ (𝑏𝐹(𝐹𝑑) ∧ 𝑎𝑁𝑏)))
2827exbii 1771 . . . . . . . . . . . . 13 (∃𝑏(𝑎𝑁𝑏𝑏𝐹(𝐹𝑑)) ↔ ∃𝑏(𝑏 ∈ dom 𝐹 ∧ (𝑏𝐹(𝐹𝑑) ∧ 𝑎𝑁𝑏)))
29 vex 3189 . . . . . . . . . . . . . 14 𝑎 ∈ V
3029, 23brco 5252 . . . . . . . . . . . . 13 (𝑎(𝐹𝑁)(𝐹𝑑) ↔ ∃𝑏(𝑎𝑁𝑏𝑏𝐹(𝐹𝑑)))
31 df-rex 2913 . . . . . . . . . . . . 13 (∃𝑏 ∈ dom 𝐹(𝑏𝐹(𝐹𝑑) ∧ 𝑎𝑁𝑏) ↔ ∃𝑏(𝑏 ∈ dom 𝐹 ∧ (𝑏𝐹(𝐹𝑑) ∧ 𝑎𝑁𝑏)))
3228, 30, 313bitr4i 292 . . . . . . . . . . . 12 (𝑎(𝐹𝑁)(𝐹𝑑) ↔ ∃𝑏 ∈ dom 𝐹(𝑏𝐹(𝐹𝑑) ∧ 𝑎𝑁𝑏))
3314ad2antrr 761 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑐𝑉𝑑𝑉)) ∧ 𝑎𝑉) ∧ (𝐹𝑎) = (𝐹𝑐)) → 𝐹 Fn 𝑉)
34 fnbrfvb 6193 . . . . . . . . . . . . . . . . . 18 ((𝐹 Fn 𝑉𝑏𝑉) → ((𝐹𝑏) = (𝐹𝑑) ↔ 𝑏𝐹(𝐹𝑑)))
3533, 34sylan 488 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑐𝑉𝑑𝑉)) ∧ 𝑎𝑉) ∧ (𝐹𝑎) = (𝐹𝑐)) ∧ 𝑏𝑉) → ((𝐹𝑏) = (𝐹𝑑) ↔ 𝑏𝐹(𝐹𝑑)))
3635anbi1d 740 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑐𝑉𝑑𝑉)) ∧ 𝑎𝑉) ∧ (𝐹𝑎) = (𝐹𝑐)) ∧ 𝑏𝑉) → (((𝐹𝑏) = (𝐹𝑑) ∧ 𝑎𝑁𝑏) ↔ (𝑏𝐹(𝐹𝑑) ∧ 𝑎𝑁𝑏)))
37 imasleval.e . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑐𝑉𝑑𝑉)) → (((𝐹𝑎) = (𝐹𝑐) ∧ (𝐹𝑏) = (𝐹𝑑)) → (𝑎𝑁𝑏𝑐𝑁𝑑)))
38373expa 1262 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎𝑉𝑏𝑉)) ∧ (𝑐𝑉𝑑𝑉)) → (((𝐹𝑎) = (𝐹𝑐) ∧ (𝐹𝑏) = (𝐹𝑑)) → (𝑎𝑁𝑏𝑐𝑁𝑑)))
3938an32s 845 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑐𝑉𝑑𝑉)) ∧ (𝑎𝑉𝑏𝑉)) → (((𝐹𝑎) = (𝐹𝑐) ∧ (𝐹𝑏) = (𝐹𝑑)) → (𝑎𝑁𝑏𝑐𝑁𝑑)))
4039anassrs 679 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑐𝑉𝑑𝑉)) ∧ 𝑎𝑉) ∧ 𝑏𝑉) → (((𝐹𝑎) = (𝐹𝑐) ∧ (𝐹𝑏) = (𝐹𝑑)) → (𝑎𝑁𝑏𝑐𝑁𝑑)))
4140impl 649 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑐𝑉𝑑𝑉)) ∧ 𝑎𝑉) ∧ 𝑏𝑉) ∧ (𝐹𝑎) = (𝐹𝑐)) ∧ (𝐹𝑏) = (𝐹𝑑)) → (𝑎𝑁𝑏𝑐𝑁𝑑))
4241pm5.32da 672 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑐𝑉𝑑𝑉)) ∧ 𝑎𝑉) ∧ 𝑏𝑉) ∧ (𝐹𝑎) = (𝐹𝑐)) → (((𝐹𝑏) = (𝐹𝑑) ∧ 𝑎𝑁𝑏) ↔ ((𝐹𝑏) = (𝐹𝑑) ∧ 𝑐𝑁𝑑)))
4342an32s 845 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑐𝑉𝑑𝑉)) ∧ 𝑎𝑉) ∧ (𝐹𝑎) = (𝐹𝑐)) ∧ 𝑏𝑉) → (((𝐹𝑏) = (𝐹𝑑) ∧ 𝑎𝑁𝑏) ↔ ((𝐹𝑏) = (𝐹𝑑) ∧ 𝑐𝑁𝑑)))
4436, 43bitr3d 270 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑐𝑉𝑑𝑉)) ∧ 𝑎𝑉) ∧ (𝐹𝑎) = (𝐹𝑐)) ∧ 𝑏𝑉) → ((𝑏𝐹(𝐹𝑑) ∧ 𝑎𝑁𝑏) ↔ ((𝐹𝑏) = (𝐹𝑑) ∧ 𝑐𝑁𝑑)))
4544rexbidva 3042 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐𝑉𝑑𝑉)) ∧ 𝑎𝑉) ∧ (𝐹𝑎) = (𝐹𝑐)) → (∃𝑏𝑉 (𝑏𝐹(𝐹𝑑) ∧ 𝑎𝑁𝑏) ↔ ∃𝑏𝑉 ((𝐹𝑏) = (𝐹𝑑) ∧ 𝑐𝑁𝑑)))
46 r19.41v 3081 . . . . . . . . . . . . . 14 (∃𝑏𝑉 ((𝐹𝑏) = (𝐹𝑑) ∧ 𝑐𝑁𝑑) ↔ (∃𝑏𝑉 (𝐹𝑏) = (𝐹𝑑) ∧ 𝑐𝑁𝑑))
4745, 46syl6bb 276 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐𝑉𝑑𝑉)) ∧ 𝑎𝑉) ∧ (𝐹𝑎) = (𝐹𝑐)) → (∃𝑏𝑉 (𝑏𝐹(𝐹𝑑) ∧ 𝑎𝑁𝑏) ↔ (∃𝑏𝑉 (𝐹𝑏) = (𝐹𝑑) ∧ 𝑐𝑁𝑑)))
4816rexeqdv 3134 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑉𝑑𝑉)) → (∃𝑏 ∈ dom 𝐹(𝑏𝐹(𝐹𝑑) ∧ 𝑎𝑁𝑏) ↔ ∃𝑏𝑉 (𝑏𝐹(𝐹𝑑) ∧ 𝑎𝑁𝑏)))
4948ad2antrr 761 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐𝑉𝑑𝑉)) ∧ 𝑎𝑉) ∧ (𝐹𝑎) = (𝐹𝑐)) → (∃𝑏 ∈ dom 𝐹(𝑏𝐹(𝐹𝑑) ∧ 𝑎𝑁𝑏) ↔ ∃𝑏𝑉 (𝑏𝐹(𝐹𝑑) ∧ 𝑎𝑁𝑏)))
50 simprr 795 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑐𝑉𝑑𝑉)) → 𝑑𝑉)
51 eqid 2621 . . . . . . . . . . . . . . . 16 (𝐹𝑑) = (𝐹𝑑)
52 fveq2 6148 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑑 → (𝐹𝑏) = (𝐹𝑑))
5352eqeq1d 2623 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑑 → ((𝐹𝑏) = (𝐹𝑑) ↔ (𝐹𝑑) = (𝐹𝑑)))
5453rspcev 3295 . . . . . . . . . . . . . . . 16 ((𝑑𝑉 ∧ (𝐹𝑑) = (𝐹𝑑)) → ∃𝑏𝑉 (𝐹𝑏) = (𝐹𝑑))
5550, 51, 54sylancl 693 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑉𝑑𝑉)) → ∃𝑏𝑉 (𝐹𝑏) = (𝐹𝑑))
5655biantrurd 529 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑉𝑑𝑉)) → (𝑐𝑁𝑑 ↔ (∃𝑏𝑉 (𝐹𝑏) = (𝐹𝑑) ∧ 𝑐𝑁𝑑)))
5756ad2antrr 761 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐𝑉𝑑𝑉)) ∧ 𝑎𝑉) ∧ (𝐹𝑎) = (𝐹𝑐)) → (𝑐𝑁𝑑 ↔ (∃𝑏𝑉 (𝐹𝑏) = (𝐹𝑑) ∧ 𝑐𝑁𝑑)))
5847, 49, 573bitr4d 300 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐𝑉𝑑𝑉)) ∧ 𝑎𝑉) ∧ (𝐹𝑎) = (𝐹𝑐)) → (∃𝑏 ∈ dom 𝐹(𝑏𝐹(𝐹𝑑) ∧ 𝑎𝑁𝑏) ↔ 𝑐𝑁𝑑))
5932, 58syl5bb 272 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐𝑉𝑑𝑉)) ∧ 𝑎𝑉) ∧ (𝐹𝑎) = (𝐹𝑐)) → (𝑎(𝐹𝑁)(𝐹𝑑) ↔ 𝑐𝑁𝑑))
6059pm5.32da 672 . . . . . . . . . 10 (((𝜑 ∧ (𝑐𝑉𝑑𝑉)) ∧ 𝑎𝑉) → (((𝐹𝑎) = (𝐹𝑐) ∧ 𝑎(𝐹𝑁)(𝐹𝑑)) ↔ ((𝐹𝑎) = (𝐹𝑐) ∧ 𝑐𝑁𝑑)))
6120, 60bitr3d 270 . . . . . . . . 9 (((𝜑 ∧ (𝑐𝑉𝑑𝑉)) ∧ 𝑎𝑉) → ((𝑎𝐹(𝐹𝑐) ∧ 𝑎(𝐹𝑁)(𝐹𝑑)) ↔ ((𝐹𝑎) = (𝐹𝑐) ∧ 𝑐𝑁𝑑)))
6261rexbidva 3042 . . . . . . . 8 ((𝜑 ∧ (𝑐𝑉𝑑𝑉)) → (∃𝑎𝑉 (𝑎𝐹(𝐹𝑐) ∧ 𝑎(𝐹𝑁)(𝐹𝑑)) ↔ ∃𝑎𝑉 ((𝐹𝑎) = (𝐹𝑐) ∧ 𝑐𝑁𝑑)))
6317, 62bitrd 268 . . . . . . 7 ((𝜑 ∧ (𝑐𝑉𝑑𝑉)) → (∃𝑎 ∈ dom 𝐹(𝑎𝐹(𝐹𝑐) ∧ 𝑎(𝐹𝑁)(𝐹𝑑)) ↔ ∃𝑎𝑉 ((𝐹𝑎) = (𝐹𝑐) ∧ 𝑐𝑁𝑑)))
64 fvex 6158 . . . . . . . . . . . 12 (𝐹𝑐) ∈ V
6564, 29brcnv 5265 . . . . . . . . . . 11 ((𝐹𝑐)𝐹𝑎𝑎𝐹(𝐹𝑐))
6665anbi1i 730 . . . . . . . . . 10 (((𝐹𝑐)𝐹𝑎𝑎(𝐹𝑁)(𝐹𝑑)) ↔ (𝑎𝐹(𝐹𝑐) ∧ 𝑎(𝐹𝑁)(𝐹𝑑)))
6729, 64breldm 5289 . . . . . . . . . . . 12 (𝑎𝐹(𝐹𝑐) → 𝑎 ∈ dom 𝐹)
6867adantr 481 . . . . . . . . . . 11 ((𝑎𝐹(𝐹𝑐) ∧ 𝑎(𝐹𝑁)(𝐹𝑑)) → 𝑎 ∈ dom 𝐹)
6968pm4.71ri 664 . . . . . . . . . 10 ((𝑎𝐹(𝐹𝑐) ∧ 𝑎(𝐹𝑁)(𝐹𝑑)) ↔ (𝑎 ∈ dom 𝐹 ∧ (𝑎𝐹(𝐹𝑐) ∧ 𝑎(𝐹𝑁)(𝐹𝑑))))
7066, 69bitri 264 . . . . . . . . 9 (((𝐹𝑐)𝐹𝑎𝑎(𝐹𝑁)(𝐹𝑑)) ↔ (𝑎 ∈ dom 𝐹 ∧ (𝑎𝐹(𝐹𝑐) ∧ 𝑎(𝐹𝑁)(𝐹𝑑))))
7170exbii 1771 . . . . . . . 8 (∃𝑎((𝐹𝑐)𝐹𝑎𝑎(𝐹𝑁)(𝐹𝑑)) ↔ ∃𝑎(𝑎 ∈ dom 𝐹 ∧ (𝑎𝐹(𝐹𝑐) ∧ 𝑎(𝐹𝑁)(𝐹𝑑))))
7264, 23brco 5252 . . . . . . . 8 ((𝐹𝑐)((𝐹𝑁) ∘ 𝐹)(𝐹𝑑) ↔ ∃𝑎((𝐹𝑐)𝐹𝑎𝑎(𝐹𝑁)(𝐹𝑑)))
73 df-rex 2913 . . . . . . . 8 (∃𝑎 ∈ dom 𝐹(𝑎𝐹(𝐹𝑐) ∧ 𝑎(𝐹𝑁)(𝐹𝑑)) ↔ ∃𝑎(𝑎 ∈ dom 𝐹 ∧ (𝑎𝐹(𝐹𝑐) ∧ 𝑎(𝐹𝑁)(𝐹𝑑))))
7471, 72, 733bitr4ri 293 . . . . . . 7 (∃𝑎 ∈ dom 𝐹(𝑎𝐹(𝐹𝑐) ∧ 𝑎(𝐹𝑁)(𝐹𝑑)) ↔ (𝐹𝑐)((𝐹𝑁) ∘ 𝐹)(𝐹𝑑))
75 r19.41v 3081 . . . . . . 7 (∃𝑎𝑉 ((𝐹𝑎) = (𝐹𝑐) ∧ 𝑐𝑁𝑑) ↔ (∃𝑎𝑉 (𝐹𝑎) = (𝐹𝑐) ∧ 𝑐𝑁𝑑))
7663, 74, 753bitr3g 302 . . . . . 6 ((𝜑 ∧ (𝑐𝑉𝑑𝑉)) → ((𝐹𝑐)((𝐹𝑁) ∘ 𝐹)(𝐹𝑑) ↔ (∃𝑎𝑉 (𝐹𝑎) = (𝐹𝑐) ∧ 𝑐𝑁𝑑)))
77 imasless.u . . . . . . . . 9 (𝜑𝑈 = (𝐹s 𝑅))
78 imasless.v . . . . . . . . 9 (𝜑𝑉 = (Base‘𝑅))
79 imasless.r . . . . . . . . 9 (𝜑𝑅𝑍)
80 imasleval.n . . . . . . . . 9 𝑁 = (le‘𝑅)
81 imasless.l . . . . . . . . 9 = (le‘𝑈)
8277, 78, 11, 79, 80, 81imasle 16104 . . . . . . . 8 (𝜑 = ((𝐹𝑁) ∘ 𝐹))
8382adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑐𝑉𝑑𝑉)) → = ((𝐹𝑁) ∘ 𝐹))
8483breqd 4624 . . . . . 6 ((𝜑 ∧ (𝑐𝑉𝑑𝑉)) → ((𝐹𝑐) (𝐹𝑑) ↔ (𝐹𝑐)((𝐹𝑁) ∘ 𝐹)(𝐹𝑑)))
85 simprl 793 . . . . . . . 8 ((𝜑 ∧ (𝑐𝑉𝑑𝑉)) → 𝑐𝑉)
86 eqid 2621 . . . . . . . 8 (𝐹𝑐) = (𝐹𝑐)
87 fveq2 6148 . . . . . . . . . 10 (𝑎 = 𝑐 → (𝐹𝑎) = (𝐹𝑐))
8887eqeq1d 2623 . . . . . . . . 9 (𝑎 = 𝑐 → ((𝐹𝑎) = (𝐹𝑐) ↔ (𝐹𝑐) = (𝐹𝑐)))
8988rspcev 3295 . . . . . . . 8 ((𝑐𝑉 ∧ (𝐹𝑐) = (𝐹𝑐)) → ∃𝑎𝑉 (𝐹𝑎) = (𝐹𝑐))
9085, 86, 89sylancl 693 . . . . . . 7 ((𝜑 ∧ (𝑐𝑉𝑑𝑉)) → ∃𝑎𝑉 (𝐹𝑎) = (𝐹𝑐))
9190biantrurd 529 . . . . . 6 ((𝜑 ∧ (𝑐𝑉𝑑𝑉)) → (𝑐𝑁𝑑 ↔ (∃𝑎𝑉 (𝐹𝑎) = (𝐹𝑐) ∧ 𝑐𝑁𝑑)))
9276, 84, 913bitr4d 300 . . . . 5 ((𝜑 ∧ (𝑐𝑉𝑑𝑉)) → ((𝐹𝑐) (𝐹𝑑) ↔ 𝑐𝑁𝑑))
9392expcom 451 . . . 4 ((𝑐𝑉𝑑𝑉) → (𝜑 → ((𝐹𝑐) (𝐹𝑑) ↔ 𝑐𝑁𝑑)))
945, 10, 93vtocl2ga 3260 . . 3 ((𝑋𝑉𝑌𝑉) → (𝜑 → ((𝐹𝑋) (𝐹𝑌) ↔ 𝑋𝑁𝑌)))
9594com12 32 . 2 (𝜑 → ((𝑋𝑉𝑌𝑉) → ((𝐹𝑋) (𝐹𝑌) ↔ 𝑋𝑁𝑌)))
96953impib 1259 1 ((𝜑𝑋𝑉𝑌𝑉) → ((𝐹𝑋) (𝐹𝑌) ↔ 𝑋𝑁𝑌))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480  ∃wex 1701   ∈ wcel 1987  ∃wrex 2908   class class class wbr 4613  ◡ccnv 5073  dom cdm 5074   ∘ ccom 5078   Fn wfn 5842  –onto→wfo 5845  ‘cfv 5847  (class class class)co 6604  Basecbs 15781  lecple 15869   “s cimas 16085 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-sup 8292  df-inf 8293  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-nn 10965  df-2 11023  df-3 11024  df-4 11025  df-5 11026  df-6 11027  df-7 11028  df-8 11029  df-9 11030  df-n0 11237  df-z 11322  df-dec 11438  df-uz 11632  df-fz 12269  df-struct 15783  df-ndx 15784  df-slot 15785  df-base 15786  df-plusg 15875  df-mulr 15876  df-sca 15878  df-vsca 15879  df-ip 15880  df-tset 15881  df-ple 15882  df-ds 15885  df-imas 16089 This theorem is referenced by:  xpsle  16162
 Copyright terms: Public domain W3C validator