Theorem bj-imdiridlem

Description: Lemma for bj-imdirid and bj-iminvid . (Contributed by BJ, 26-May-2024)

	Ref	Expression
Hypothesis	bj-imdiridlem.1	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴 ) → ( 𝜑 ↔ 𝑥 = 𝑦 ) )
Assertion	bj-imdiridlem	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝜑 ) } = ( I ↾ 𝒫 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		bj-imdiridlem.1	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴 ) → ( 𝜑 ↔ 𝑥 = 𝑦 ) )
2	1	biimp3a	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝑦 )
3	2	3expib	⊢ ( 𝑥 ⊆ 𝐴 → ( ( 𝑦 ⊆ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝑦 ) )
4		equcomi	⊢ ( 𝑥 = 𝑦 → 𝑦 = 𝑥 )
5	4	sseq1d	⊢ ( 𝑥 = 𝑦 → ( 𝑦 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐴 ) )
6	5	biimparc	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦 ) → 𝑦 ⊆ 𝐴 )
7		simpr	⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦 ) ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ⊆ 𝐴 )
8	1	biimpar	⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑥 = 𝑦 ) → 𝜑 )
9	8	an32s	⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦 ) ∧ 𝑦 ⊆ 𝐴 ) → 𝜑 )
10	7 9	jca	⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦 ) ∧ 𝑦 ⊆ 𝐴 ) → ( 𝑦 ⊆ 𝐴 ∧ 𝜑 ) )
11	6 10	mpdan	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦 ) → ( 𝑦 ⊆ 𝐴 ∧ 𝜑 ) )
12	11	ex	⊢ ( 𝑥 ⊆ 𝐴 → ( 𝑥 = 𝑦 → ( 𝑦 ⊆ 𝐴 ∧ 𝜑 ) ) )
13	3 12	impbid	⊢ ( 𝑥 ⊆ 𝐴 → ( ( 𝑦 ⊆ 𝐴 ∧ 𝜑 ) ↔ 𝑥 = 𝑦 ) )
14	13	pm5.32i	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝜑 ) ) ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦 ) )
15		anass	⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝜑 ) ↔ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝜑 ) ) )
16		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
17		vex	⊢ 𝑦 ∈ V
18	17	ideq	⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
19	16 18	anbi12i	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 I 𝑦 ) ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦 ) )
20	14 15 19	3bitr4i	⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 I 𝑦 ) )
21	20	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝜑 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 I 𝑦 ) }
22		dfres2	⊢ ( I ↾ 𝒫 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 I 𝑦 ) }
23	21 22	eqtr4i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝜑 ) } = ( I ↾ 𝒫 𝐴 )