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) Use ax-pr instead. (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | axpr | ⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | axprlem3 | ⊢ ∃ 𝑧 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) | |
| 2 | biimpr | ⊢ ( ( 𝑤 ∈ 𝑧 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) → ( ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) → 𝑤 ∈ 𝑧 ) ) | |
| 3 | 2 | alimi | ⊢ ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) → ∀ 𝑤 ( ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) → 𝑤 ∈ 𝑧 ) ) |
| 4 | 1 3 | eximii | ⊢ ∃ 𝑧 ∀ 𝑤 ( ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) → 𝑤 ∈ 𝑧 ) |
| 5 | axprlem4 | ⊢ ( ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) ∧ 𝑤 = 𝑥 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) | |
| 6 | axprlem5 | ⊢ ( ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) ∧ 𝑤 = 𝑦 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) | |
| 7 | 5 6 | jaodan | ⊢ ( ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) ∧ ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) |
| 8 | 7 | ex | ⊢ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) → ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) ) |
| 9 | 8 | imim1d | ⊢ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) → ( ( ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) → 𝑤 ∈ 𝑧 ) → ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ) ) |
| 10 | 9 | alimdv | ⊢ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) → ( ∀ 𝑤 ( ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) → 𝑤 ∈ 𝑧 ) → ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ) ) |
| 11 | 10 | eximdv | ⊢ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) → ( ∃ 𝑧 ∀ 𝑤 ( ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) → 𝑤 ∈ 𝑧 ) → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ) ) |
| 12 | 4 11 | mpi | ⊢ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) → ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) ) |
| 13 | axprlem2 | ⊢ ∃ 𝑝 ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) | |
| 14 | 12 13 | exlimiiv | ⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 ∈ 𝑧 ) |