Description: The "Godel-set for the Sheffer stroke NAND" for two formulas A and B . (Contributed by AV, 16-Oct-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | gonafv | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ⊼𝑔 𝐵 ) = 〈 1o , 〈 𝐴 , 𝐵 〉 〉 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ov | ⊢ ( 𝐴 ⊼𝑔 𝐵 ) = ( ⊼𝑔 ‘ 〈 𝐴 , 𝐵 〉 ) | |
2 | opelvvg | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 〈 𝐴 , 𝐵 〉 ∈ ( V × V ) ) | |
3 | opeq2 | ⊢ ( 𝑥 = 〈 𝐴 , 𝐵 〉 → 〈 1o , 𝑥 〉 = 〈 1o , 〈 𝐴 , 𝐵 〉 〉 ) | |
4 | df-gona | ⊢ ⊼𝑔 = ( 𝑥 ∈ ( V × V ) ↦ 〈 1o , 𝑥 〉 ) | |
5 | opex | ⊢ 〈 1o , 〈 𝐴 , 𝐵 〉 〉 ∈ V | |
6 | 3 4 5 | fvmpt | ⊢ ( 〈 𝐴 , 𝐵 〉 ∈ ( V × V ) → ( ⊼𝑔 ‘ 〈 𝐴 , 𝐵 〉 ) = 〈 1o , 〈 𝐴 , 𝐵 〉 〉 ) |
7 | 2 6 | syl | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⊼𝑔 ‘ 〈 𝐴 , 𝐵 〉 ) = 〈 1o , 〈 𝐴 , 𝐵 〉 〉 ) |
8 | 1 7 | syl5eq | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ⊼𝑔 𝐵 ) = 〈 1o , 〈 𝐴 , 𝐵 〉 〉 ) |