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 ⊢ 𝐹 = ( 𝑥 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑥 ‘ 0 ) 𝑂 ( 𝑥 ‘ 1 ) ) )
Assertion 2arymptfv ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ) = ( 𝐴 𝑂 𝐵 ) )

Proof

Step Hyp Ref Expression
1 2arympt.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑥 ‘ 0 ) 𝑂 ( 𝑥 ‘ 1 ) ) )
2 fveq1 ⊢ ( 𝑥 = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } → ( 𝑥 ‘ 0 ) = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ‘ 0 ) )
3 2 adantl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑥 = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ) → ( 𝑥 ‘ 0 ) = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ‘ 0 ) )
4 c0ex ⊢ 0 ∈ V
5 4 a1i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 0 ∈ V )
6 simp2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
7 0ne1 ⊢ 0 ≠ 1
8 7 a1i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 0 ≠ 1 )
9 5 6 8 3jca ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 0 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 0 ≠ 1 ) )
10 9 adantr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑥 = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ) → ( 0 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 0 ≠ 1 ) )
11 fvpr1g ⊢ ( ( 0 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 0 ≠ 1 ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ‘ 0 ) = 𝐴 )
12 10 11 syl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑥 = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ‘ 0 ) = 𝐴 )
13 3 12 eqtrd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑥 = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ) → ( 𝑥 ‘ 0 ) = 𝐴 )
14 fveq1 ⊢ ( 𝑥 = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } → ( 𝑥 ‘ 1 ) = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ‘ 1 ) )
15 1ex ⊢ 1 ∈ V
16 simp3 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
17 fvpr2g ⊢ ( ( 1 ∈ V ∧ 𝐵 ∈ 𝑋 ∧ 0 ≠ 1 ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ‘ 1 ) = 𝐵 )
18 15 16 8 17 mp3an2i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ‘ 1 ) = 𝐵 )
19 14 18 sylan9eqr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑥 = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ) → ( 𝑥 ‘ 1 ) = 𝐵 )
20 13 19 oveq12d ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑥 = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ) → ( ( 𝑥 ‘ 0 ) 𝑂 ( 𝑥 ‘ 1 ) ) = ( 𝐴 𝑂 𝐵 ) )
21 simp1 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑋 ∈ 𝑉 )
22 4 15 7 3pm3.2i ⊢ ( 0 ∈ V ∧ 1 ∈ V ∧ 0 ≠ 1 )
23 22 a1i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 0 ∈ V ∧ 1 ∈ V ∧ 0 ≠ 1 ) )
24 3simpc ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) )
25 fprmappr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 0 ∈ V ∧ 1 ∈ V ∧ 0 ≠ 1 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∈ ( 𝑋 ↑m { 0 , 1 } ) )
26 21 23 24 25 syl3anc ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∈ ( 𝑋 ↑m { 0 , 1 } ) )
27 ovexd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑂 𝐵 ) ∈ V )
28 1 20 26 27 fvmptd2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ) = ( 𝐴 𝑂 𝐵 ) )