Step |
Hyp |
Ref |
Expression |
1 |
|
peano1 |
⊢ ∅ ∈ ω |
2 |
1
|
a1i |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∅ ∈ ω ) |
3 |
|
1onn |
⊢ 1o ∈ ω |
4 |
3
|
a1i |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 1o ∈ ω ) |
5 |
|
simpl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐴 ∈ 𝑉 ) |
6 |
|
simpr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐵 ∈ 𝑊 ) |
7 |
|
1n0 |
⊢ 1o ≠ ∅ |
8 |
7
|
necomi |
⊢ ∅ ≠ 1o |
9 |
8
|
a1i |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∅ ≠ 1o ) |
10 |
|
fnprg |
⊢ ( ( ( ∅ ∈ ω ∧ 1o ∈ ω ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ∅ ≠ 1o ) → { 〈 ∅ , 𝐴 〉 , 〈 1o , 𝐵 〉 } Fn { ∅ , 1o } ) |
11 |
2 4 5 6 9 10
|
syl221anc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { 〈 ∅ , 𝐴 〉 , 〈 1o , 𝐵 〉 } Fn { ∅ , 1o } ) |
12 |
|
df2o3 |
⊢ 2o = { ∅ , 1o } |
13 |
12
|
fneq2i |
⊢ ( { 〈 ∅ , 𝐴 〉 , 〈 1o , 𝐵 〉 } Fn 2o ↔ { 〈 ∅ , 𝐴 〉 , 〈 1o , 𝐵 〉 } Fn { ∅ , 1o } ) |
14 |
11 13
|
sylibr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { 〈 ∅ , 𝐴 〉 , 〈 1o , 𝐵 〉 } Fn 2o ) |