Theorem coi1in

Description: Precomposition with the identity expressed as intersection. (Contributed by BJ, 16-Aug-2026)

	Ref	Expression
Assertion	coi1in	⊢ ( 𝐴 ∘ I ) = ( 𝐴 ∩ ( V × V ) )

Proof

Step	Hyp	Ref	Expression
1		19.42vv	⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ V ∧ 𝑧 ∈ V ) ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ V ∧ 𝑧 ∈ V ) ) ) )
2		vex	⊢ 𝑡 ∈ V
3	2	ideq	⊢ ( 𝑦 I 𝑡 ↔ 𝑦 = 𝑡 )
4	3	anbi1i	⊢ ( ( 𝑦 I 𝑡 ∧ 𝑡 𝐴 𝑧 ) ↔ ( 𝑦 = 𝑡 ∧ 𝑡 𝐴 𝑧 ) )
5		equcomi	⊢ ( 𝑦 = 𝑡 → 𝑡 = 𝑦 )
6	5	breq1d	⊢ ( 𝑦 = 𝑡 → ( 𝑡 𝐴 𝑧 ↔ 𝑦 𝐴 𝑧 ) )
7	6	pm5.32i	⊢ ( ( 𝑦 = 𝑡 ∧ 𝑡 𝐴 𝑧 ) ↔ ( 𝑦 = 𝑡 ∧ 𝑦 𝐴 𝑧 ) )
8	4 7	bitri	⊢ ( ( 𝑦 I 𝑡 ∧ 𝑡 𝐴 𝑧 ) ↔ ( 𝑦 = 𝑡 ∧ 𝑦 𝐴 𝑧 ) )
9	8	exbii	⊢ ( ∃ 𝑡 ( 𝑦 I 𝑡 ∧ 𝑡 𝐴 𝑧 ) ↔ ∃ 𝑡 ( 𝑦 = 𝑡 ∧ 𝑦 𝐴 𝑧 ) )
10		ax6evr	⊢ ∃ 𝑡 𝑦 = 𝑡
11		19.41v	⊢ ( ∃ 𝑡 ( 𝑦 = 𝑡 ∧ 𝑦 𝐴 𝑧 ) ↔ ( ∃ 𝑡 𝑦 = 𝑡 ∧ 𝑦 𝐴 𝑧 ) )
12	10 11	mpbiran	⊢ ( ∃ 𝑡 ( 𝑦 = 𝑡 ∧ 𝑦 𝐴 𝑧 ) ↔ 𝑦 𝐴 𝑧 )
13		df-br	⊢ ( 𝑦 𝐴 𝑧 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 )
14	9 12 13	3bitri	⊢ ( ∃ 𝑡 ( 𝑦 I 𝑡 ∧ 𝑡 𝐴 𝑧 ) ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 )
15		eleq1	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑥 ∈ 𝐴 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 ) )
16	14 15	bitr4id	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( ∃ 𝑡 ( 𝑦 I 𝑡 ∧ 𝑡 𝐴 𝑧 ) ↔ 𝑥 ∈ 𝐴 ) )
17	16	pm5.32i	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ∃ 𝑡 ( 𝑦 I 𝑡 ∧ 𝑡 𝐴 𝑧 ) ) ↔ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑥 ∈ 𝐴 ) )
18	17	biancomi	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ∃ 𝑡 ( 𝑦 I 𝑡 ∧ 𝑡 𝐴 𝑧 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ) )
19		vex	⊢ 𝑦 ∈ V
20		vex	⊢ 𝑧 ∈ V
21	19 20	pm3.2i	⊢ ( 𝑦 ∈ V ∧ 𝑧 ∈ V )
22	21	biantru	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( 𝑦 ∈ V ∧ 𝑧 ∈ V ) ) )
23		anass	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( 𝑦 ∈ V ∧ 𝑧 ∈ V ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ V ∧ 𝑧 ∈ V ) ) ) )
24	18 22 23	3bitri	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ∃ 𝑡 ( 𝑦 I 𝑡 ∧ 𝑡 𝐴 𝑧 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ V ∧ 𝑧 ∈ V ) ) ) )
25	24	exbii	⊢ ( ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ∃ 𝑡 ( 𝑦 I 𝑡 ∧ 𝑡 𝐴 𝑧 ) ) ↔ ∃ 𝑧 ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ V ∧ 𝑧 ∈ V ) ) ) )
26	25	exbii	⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ∃ 𝑡 ( 𝑦 I 𝑡 ∧ 𝑡 𝐴 𝑧 ) ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ V ∧ 𝑧 ∈ V ) ) ) )
27		elxp	⊢ ( 𝑥 ∈ ( V × V ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ V ∧ 𝑧 ∈ V ) ) )
28	27	anbi2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( V × V ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ V ∧ 𝑧 ∈ V ) ) ) )
29	1 26 28	3bitr4i	⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ∃ 𝑡 ( 𝑦 I 𝑡 ∧ 𝑡 𝐴 𝑧 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( V × V ) ) )
30		elco	⊢ ( 𝑥 ∈ ( 𝐴 ∘ I ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ∃ 𝑡 ( 𝑦 I 𝑡 ∧ 𝑡 𝐴 𝑧 ) ) )
31		elin	⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( V × V ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( V × V ) ) )
32	29 30 31	3bitr4i	⊢ ( 𝑥 ∈ ( 𝐴 ∘ I ) ↔ 𝑥 ∈ ( 𝐴 ∩ ( V × V ) ) )
33	32	eqriv	⊢ ( 𝐴 ∘ I ) = ( 𝐴 ∩ ( V × V ) )