Metamath Proof Explorer

Theorem 2arympt

Description: 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 2arympt ⊢ X ∈ V ∧ O : X × X ⟶ X → F ∈ 2 -aryF X

Proof

Step Hyp Ref Expression
1 2arympt.f ⊢ F = x ∈ X 0 1 ⟼ x ⁡ 0 O x ⁡ 1
2 simplr ⊢ X ∈ V ∧ O : X × X ⟶ X ∧ x ∈ X 0 1 → O : X × X ⟶ X
3 elmapi ⊢ x ∈ X 0 1 → x : 0 1 ⟶ X
4 c0ex ⊢ 0 ∈ V
5 4 prid1 ⊢ 0 ∈ 0 1
6 5 a1i ⊢ x ∈ X 0 1 → 0 ∈ 0 1
7 3 6 ffvelcdmd ⊢ x ∈ X 0 1 → x ⁡ 0 ∈ X
8 7 adantl ⊢ X ∈ V ∧ O : X × X ⟶ X ∧ x ∈ X 0 1 → x ⁡ 0 ∈ X
9 1ex ⊢ 1 ∈ V
10 9 prid2 ⊢ 1 ∈ 0 1
11 10 a1i ⊢ x ∈ X 0 1 → 1 ∈ 0 1
12 3 11 ffvelcdmd ⊢ x ∈ X 0 1 → x ⁡ 1 ∈ X
13 12 adantl ⊢ X ∈ V ∧ O : X × X ⟶ X ∧ x ∈ X 0 1 → x ⁡ 1 ∈ X
14 2 8 13 fovcdmd ⊢ X ∈ V ∧ O : X × X ⟶ X ∧ x ∈ X 0 1 → x ⁡ 0 O x ⁡ 1 ∈ X
15 14 1 fmptd ⊢ X ∈ V ∧ O : X × X ⟶ X → F : X 0 1 ⟶ X
16 2aryfvalel ⊢ X ∈ V → F ∈ 2 -aryF X ↔ F : X 0 1 ⟶ X
17 16 adantr ⊢ X ∈ V ∧ O : X × X ⟶ X → F ∈ 2 -aryF X ↔ F : X 0 1 ⟶ X
18 15 17 mpbird ⊢ X ∈ V ∧ O : X × X ⟶ X → F ∈ 2 -aryF X