Metamath Proof Explorer

Theorem axpr

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 ⊢ ∃ z ∀ w w = x ∨ w = y → w ∈ z

Proof

Step Hyp Ref Expression
1 axprlem3 ⊢ ∃ z ∀ w w ∈ z ↔ ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
2 axprlem1 ⊢ ∃ s ∀ n ∀ t ¬ t ∈ n → n ∈ s
3 2 sepexi ⊢ ∃ s ∀ n n ∈ s ↔ ∀ t ¬ t ∈ n
4 biimp ⊢ n ∈ s ↔ ∀ t ¬ t ∈ n → n ∈ s → ∀ t ¬ t ∈ n
5 ax-nul ⊢ ∃ n ∀ t ¬ t ∈ n
6 exbi ⊢ ∀ n n ∈ s ↔ ∀ t ¬ t ∈ n → ∃ n n ∈ s ↔ ∃ n ∀ t ¬ t ∈ n
7 5 6 mpbiri ⊢ ∀ n n ∈ s ↔ ∀ t ¬ t ∈ n → ∃ n n ∈ s
8 ifptru ⊢ ∃ n n ∈ s → if- ∃ n n ∈ s w = x w = y ↔ w = x
9 7 8 syl ⊢ ∀ n n ∈ s ↔ ∀ t ¬ t ∈ n → if- ∃ n n ∈ s w = x w = y ↔ w = x
10 3 4 9 axprlem4 ⊢ ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p → w = x → ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
11 ax-nul ⊢ ∃ s ∀ n ¬ n ∈ s
12 pm2.21 ⊢ ¬ n ∈ s → n ∈ s → ∀ t ¬ t ∈ n
13 alnex ⊢ ∀ n ¬ n ∈ s ↔ ¬ ∃ n n ∈ s
14 ifpfal ⊢ ¬ ∃ n n ∈ s → if- ∃ n n ∈ s w = x w = y ↔ w = y
15 13 14 sylbi ⊢ ∀ n ¬ n ∈ s → if- ∃ n n ∈ s w = x w = y ↔ w = y
16 11 12 15 axprlem4 ⊢ ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p → w = y → ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
17 10 16 jaod ⊢ ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p → w = x ∨ w = y → ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
18 imbi2 ⊢ w ∈ z ↔ ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y → w = x ∨ w = y → w ∈ z ↔ w = x ∨ w = y → ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
19 17 18 syl5ibrcom ⊢ ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p → w ∈ z ↔ ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y → w = x ∨ w = y → w ∈ z
20 19 alimdv ⊢ ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p → ∀ w w ∈ z ↔ ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y → ∀ w w = x ∨ w = y → w ∈ z
21 20 eximdv ⊢ ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p → ∃ z ∀ w w ∈ z ↔ ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y → ∃ z ∀ w w = x ∨ w = y → w ∈ z
22 1 21 mpi ⊢ ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p → ∃ z ∀ w w = x ∨ w = y → w ∈ z
23 axprlem2 ⊢ ∃ p ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p
24 22 23 exlimiiv ⊢ ∃ z ∀ w w = x ∨ w = y → w ∈ z