Metamath Proof Explorer


Theorem sdom1

Description: A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 12-Dec-2024)

Ref Expression
Assertion sdom1 A 1 𝑜 A =

Proof

Step Hyp Ref Expression
1 df1o2 1 𝑜 =
2 1 breq2i A 1 𝑜 A
3 brdomi A f f : A 1-1
4 f1cdmsn f : A 1-1 A x A = x
5 vex x V
6 5 ensn1 x 1 𝑜
7 breq1 A = x A 1 𝑜 x 1 𝑜
8 6 7 mpbiri A = x A 1 𝑜
9 8 exlimiv x A = x A 1 𝑜
10 4 9 syl f : A 1-1 A A 1 𝑜
11 10 expcom A f : A 1-1 A 1 𝑜
12 11 exlimdv A f f : A 1-1 A 1 𝑜
13 3 12 syl5 A A A 1 𝑜
14 2 13 biimtrid A A 1 𝑜 A 1 𝑜
15 iman A 1 𝑜 A 1 𝑜 ¬ A 1 𝑜 ¬ A 1 𝑜
16 14 15 sylib A ¬ A 1 𝑜 ¬ A 1 𝑜
17 brsdom A 1 𝑜 A 1 𝑜 ¬ A 1 𝑜
18 16 17 sylnibr A ¬ A 1 𝑜
19 18 necon4ai A 1 𝑜 A =
20 1n0 1 𝑜
21 1oex 1 𝑜 V
22 21 0sdom 1 𝑜 1 𝑜
23 20 22 mpbir 1 𝑜
24 breq1 A = A 1 𝑜 1 𝑜
25 23 24 mpbiri A = A 1 𝑜
26 19 25 impbii A 1 𝑜 A =