Description: Unabbreviated version of the Axiom of Pairing of ZF set theory, derived as a theorem from the other axioms.
This theorem should not be referenced by any proof. Instead, use ax-pr below so that the uses of the Axiom of Pairing can be more easily identified.
For a shorter proof using ax-ext , see axprALT . (Contributed by NM, 14-Nov-2006) Remove dependency on ax-ext . (Revised by Rohan Ridenour, 10-Aug-2023) (Proof shortened by BJ, 13-Aug-2023) (Proof shortened by Matthew House, 18-Sep-2025) Use ax-pr instead. (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | axpr | |- E. z A. w ( ( w = x \/ w = y ) -> w e. z ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | axprlem3 | |- E. z A. w ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) |
|
| 2 | axprlem1 | |- E. s A. n ( A. t -. t e. n -> n e. s ) |
|
| 3 | 2 | sepexi | |- E. s A. n ( n e. s <-> A. t -. t e. n ) |
| 4 | biimp | |- ( ( n e. s <-> A. t -. t e. n ) -> ( n e. s -> A. t -. t e. n ) ) |
|
| 5 | ax-nul | |- E. n A. t -. t e. n |
|
| 6 | exbi | |- ( A. n ( n e. s <-> A. t -. t e. n ) -> ( E. n n e. s <-> E. n A. t -. t e. n ) ) |
|
| 7 | 5 6 | mpbiri | |- ( A. n ( n e. s <-> A. t -. t e. n ) -> E. n n e. s ) |
| 8 | ifptru | |- ( E. n n e. s -> ( if- ( E. n n e. s , w = x , w = y ) <-> w = x ) ) |
|
| 9 | 7 8 | syl | |- ( A. n ( n e. s <-> A. t -. t e. n ) -> ( if- ( E. n n e. s , w = x , w = y ) <-> w = x ) ) |
| 10 | 3 4 9 | axprlem4 | |- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( w = x -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) ) |
| 11 | ax-nul | |- E. s A. n -. n e. s |
|
| 12 | pm2.21 | |- ( -. n e. s -> ( n e. s -> A. t -. t e. n ) ) |
|
| 13 | alnex | |- ( A. n -. n e. s <-> -. E. n n e. s ) |
|
| 14 | ifpfal | |- ( -. E. n n e. s -> ( if- ( E. n n e. s , w = x , w = y ) <-> w = y ) ) |
|
| 15 | 13 14 | sylbi | |- ( A. n -. n e. s -> ( if- ( E. n n e. s , w = x , w = y ) <-> w = y ) ) |
| 16 | 11 12 15 | axprlem4 | |- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( w = y -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) ) |
| 17 | 10 16 | jaod | |- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( ( w = x \/ w = y ) -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) ) |
| 18 | imbi2 | |- ( ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) -> ( ( ( w = x \/ w = y ) -> w e. z ) <-> ( ( w = x \/ w = y ) -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) ) ) |
|
| 19 | 17 18 | syl5ibrcom | |- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) -> ( ( w = x \/ w = y ) -> w e. z ) ) ) |
| 20 | 19 | alimdv | |- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( A. w ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) -> A. w ( ( w = x \/ w = y ) -> w e. z ) ) ) |
| 21 | 20 | eximdv | |- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( E. z A. w ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) -> E. z A. w ( ( w = x \/ w = y ) -> w e. z ) ) ) |
| 22 | 1 21 | mpi | |- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> E. z A. w ( ( w = x \/ w = y ) -> w e. z ) ) |
| 23 | axprlem2 | |- E. p A. s ( A. n e. s A. t -. t e. n -> s e. p ) |
|
| 24 | 22 23 | exlimiiv | |- E. z A. w ( ( w = x \/ w = y ) -> w e. z ) |