Metamath Proof Explorer


Theorem 2arymptfv

Description: The value of a binary (endo)function in maps-to notation. (Contributed by AV, 20-May-2024)

Ref Expression
Hypothesis 2arympt.f F = x X 0 1 x 0 O x 1
Assertion 2arymptfv X V A X B X F 0 A 1 B = A O B

Proof

Step Hyp Ref Expression
1 2arympt.f F = x X 0 1 x 0 O x 1
2 fveq1 x = 0 A 1 B x 0 = 0 A 1 B 0
3 2 adantl X V A X B X x = 0 A 1 B x 0 = 0 A 1 B 0
4 c0ex 0 V
5 4 a1i X V A X B X 0 V
6 simp2 X V A X B X A X
7 0ne1 0 1
8 7 a1i X V A X B X 0 1
9 5 6 8 3jca X V A X B X 0 V A X 0 1
10 9 adantr X V A X B X x = 0 A 1 B 0 V A X 0 1
11 fvpr1g 0 V A X 0 1 0 A 1 B 0 = A
12 10 11 syl X V A X B X x = 0 A 1 B 0 A 1 B 0 = A
13 3 12 eqtrd X V A X B X x = 0 A 1 B x 0 = A
14 fveq1 x = 0 A 1 B x 1 = 0 A 1 B 1
15 1ex 1 V
16 simp3 X V A X B X B X
17 fvpr2g 1 V B X 0 1 0 A 1 B 1 = B
18 15 16 8 17 mp3an2i X V A X B X 0 A 1 B 1 = B
19 14 18 sylan9eqr X V A X B X x = 0 A 1 B x 1 = B
20 13 19 oveq12d X V A X B X x = 0 A 1 B x 0 O x 1 = A O B
21 simp1 X V A X B X X V
22 4 15 7 3pm3.2i 0 V 1 V 0 1
23 22 a1i X V A X B X 0 V 1 V 0 1
24 3simpc X V A X B X A X B X
25 fprmappr X V 0 V 1 V 0 1 A X B X 0 A 1 B X 0 1
26 21 23 24 25 syl3anc X V A X B X 0 A 1 B X 0 1
27 ovexd X V A X B X A O B V
28 1 20 26 27 fvmptd2 X V A X B X F 0 A 1 B = A O B