Description: Existence of the result of the adjunction (generalized only in the first term since this suffices for current applications). (Contributed by BJ, 19-Jan-2025) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-adjg1 | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∪ { 𝑥 } ) ∈ V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | uneq1 | ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∪ { 𝑥 } ) = ( 𝐴 ∪ { 𝑥 } ) ) | |
| 2 | 1 | eleq1d | ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ∪ { 𝑥 } ) ∈ V ↔ ( 𝐴 ∪ { 𝑥 } ) ∈ V ) ) |
| 3 | ax-bj-adj | ⊢ ∀ 𝑦 ∀ 𝑥 ∃ 𝑧 ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ ( 𝑡 ∈ 𝑦 ∨ 𝑡 = 𝑥 ) ) | |
| 4 | 3 | spi | ⊢ ∀ 𝑥 ∃ 𝑧 ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ ( 𝑡 ∈ 𝑦 ∨ 𝑡 = 𝑥 ) ) |
| 5 | 4 | spi | ⊢ ∃ 𝑧 ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ ( 𝑡 ∈ 𝑦 ∨ 𝑡 = 𝑥 ) ) |
| 6 | bj-axadj | ⊢ ( ( 𝑦 ∪ { 𝑥 } ) ∈ V ↔ ∃ 𝑧 ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ ( 𝑡 ∈ 𝑦 ∨ 𝑡 = 𝑥 ) ) ) | |
| 7 | 5 6 | mpbir | ⊢ ( 𝑦 ∪ { 𝑥 } ) ∈ V |
| 8 | 2 7 | vtoclg | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∪ { 𝑥 } ) ∈ V ) |