Axiom ax-bj-adj

Description: Axiom of adjunction. (Contributed by BJ, 19-Jan-2025)

	Ref	Expression
Assertion	ax-bj-adj	⊢ ∀ 𝑥 ∀ 𝑦 ∃ 𝑧 ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ ( 𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		vy	⊢ 𝑦
2		vz	⊢ 𝑧
3		vt	⊢ 𝑡
4	3	cv	⊢ 𝑡
5	2	cv	⊢ 𝑧
6	4 5	wcel	⊢ 𝑡 ∈ 𝑧
7	0	cv	⊢ 𝑥
8	4 7	wcel	⊢ 𝑡 ∈ 𝑥
9	1	cv	⊢ 𝑦
10	4 9	wceq	⊢ 𝑡 = 𝑦
11	8 10	wo	⊢ ( 𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦 )
12	6 11	wb	⊢ ( 𝑡 ∈ 𝑧 ↔ ( 𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦 ) )
13	12 3	wal	⊢ ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ ( 𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦 ) )
14	13 2	wex	⊢ ∃ 𝑧 ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ ( 𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦 ) )
15	14 1	wal	⊢ ∀ 𝑦 ∃ 𝑧 ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ ( 𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦 ) )
16	15 0	wal	⊢ ∀ 𝑥 ∀ 𝑦 ∃ 𝑧 ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ ( 𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦 ) )