Metamath Proof Explorer


Theorem enpr2dOLD

Description: Obsolete version of enpr2d as of 23-Dec-2024. (Contributed by Rohan Ridenour, 3-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses enpr2dOLD.1 φ A C
enpr2dOLD.2 φ B D
enpr2dOLD.3 φ ¬ A = B
Assertion enpr2dOLD φ A B 2 𝑜

Proof

Step Hyp Ref Expression
1 enpr2dOLD.1 φ A C
2 enpr2dOLD.2 φ B D
3 enpr2dOLD.3 φ ¬ A = B
4 ensn1g A C A 1 𝑜
5 1 4 syl φ A 1 𝑜
6 1on 1 𝑜 On
7 en2sn B D 1 𝑜 On B 1 𝑜
8 2 6 7 sylancl φ B 1 𝑜
9 3 neqned φ A B
10 disjsn2 A B A B =
11 9 10 syl φ A B =
12 6 onirri ¬ 1 𝑜 1 𝑜
13 12 a1i φ ¬ 1 𝑜 1 𝑜
14 disjsn 1 𝑜 1 𝑜 = ¬ 1 𝑜 1 𝑜
15 13 14 sylibr φ 1 𝑜 1 𝑜 =
16 unen A 1 𝑜 B 1 𝑜 A B = 1 𝑜 1 𝑜 = A B 1 𝑜 1 𝑜
17 5 8 11 15 16 syl22anc φ A B 1 𝑜 1 𝑜
18 df-pr A B = A B
19 df-suc suc 1 𝑜 = 1 𝑜 1 𝑜
20 17 18 19 3brtr4g φ A B suc 1 𝑜
21 df-2o 2 𝑜 = suc 1 𝑜
22 20 21 breqtrrdi φ A B 2 𝑜