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 | ⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | axprlem3 | ⊢ ∃ 𝑧 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) | |
| 2 | axprlem1 | ⊢ ∃ 𝑠 ∀ 𝑛 ( ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑛 ∈ 𝑠 ) | |
| 3 | 2 | sepexi | ⊢ ∃ 𝑠 ∀ 𝑛 ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) |
| 4 | biimp | ⊢ ( ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) → ( 𝑛 ∈ 𝑠 → ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) ) | |
| 5 | ax-nul | ⊢ ∃ 𝑛 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 | |
| 6 | exbi | ⊢ ( ∀ 𝑛 ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) → ( ∃ 𝑛 𝑛 ∈ 𝑠 ↔ ∃ 𝑛 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) ) | |
| 7 | 5 6 | mpbiri | ⊢ ( ∀ 𝑛 ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) → ∃ 𝑛 𝑛 ∈ 𝑠 ) |
| 8 | ifptru | ⊢ ( ∃ 𝑛 𝑛 ∈ 𝑠 → ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ↔ 𝑤 = 𝑥 ) ) | |
| 9 | 7 8 | syl | ⊢ ( ∀ 𝑛 ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) → ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ↔ 𝑤 = 𝑥 ) ) |
| 10 | 3 4 9 | axprlem4 | ⊢ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) → ( 𝑤 = 𝑥 → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) ) |
| 11 | ax-nul | ⊢ ∃ 𝑠 ∀ 𝑛 ¬ 𝑛 ∈ 𝑠 | |
| 12 | pm2.21 | ⊢ ( ¬ 𝑛 ∈ 𝑠 → ( 𝑛 ∈ 𝑠 → ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) ) | |
| 13 | alnex | ⊢ ( ∀ 𝑛 ¬ 𝑛 ∈ 𝑠 ↔ ¬ ∃ 𝑛 𝑛 ∈ 𝑠 ) | |
| 14 | ifpfal | ⊢ ( ¬ ∃ 𝑛 𝑛 ∈ 𝑠 → ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ↔ 𝑤 = 𝑦 ) ) | |
| 15 | 13 14 | sylbi | ⊢ ( ∀ 𝑛 ¬ 𝑛 ∈ 𝑠 → ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ↔ 𝑤 = 𝑦 ) ) |
| 16 | 11 12 15 | axprlem4 | ⊢ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) → ( 𝑤 = 𝑦 → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) ) |
| 17 | 10 16 | jaod | ⊢ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) → ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) ) |
| 18 | imbi2 | ⊢ ( ( 𝑤 ∈ 𝑧 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) → ( ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ↔ ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) ) ) | |
| 19 | 17 18 | syl5ibrcom | ⊢ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) → ( ( 𝑤 ∈ 𝑧 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) → ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ) ) |
| 20 | 19 | alimdv | ⊢ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) → ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) → ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ) ) |
| 21 | 20 | eximdv | ⊢ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) → ( ∃ 𝑧 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ) ) |
| 22 | 1 21 | mpi | ⊢ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ) |
| 23 | axprlem2 | ⊢ ∃ 𝑝 ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) | |
| 24 | 22 23 | exlimiiv | ⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) |