Theorem idfudiag1lem

Description: Lemma for idfudiag1bas and idfudiag1 . (Contributed by Zhi Wang, 19-Oct-2025)

	Ref	Expression
Hypotheses	idfudiag1lem.1	⊢ ( 𝜑 → ( I ↾ 𝐴 ) = ( 𝐴 × { 𝐵 } ) )
	idfudiag1lem.2	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
Assertion	idfudiag1lem	⊢ ( 𝜑 → 𝐴 = { 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		idfudiag1lem.1	⊢ ( 𝜑 → ( I ↾ 𝐴 ) = ( 𝐴 × { 𝐵 } ) )
2		idfudiag1lem.2	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
3		rnresi	⊢ ran ( I ↾ 𝐴 ) = 𝐴
4	1	rneqd	⊢ ( 𝜑 → ran ( I ↾ 𝐴 ) = ran ( 𝐴 × { 𝐵 } ) )
5	3 4	eqtr3id	⊢ ( 𝜑 → 𝐴 = ran ( 𝐴 × { 𝐵 } ) )
6		rnxp	⊢ ( 𝐴 ≠ ∅ → ran ( 𝐴 × { 𝐵 } ) = { 𝐵 } )
7	2 6	syl	⊢ ( 𝜑 → ran ( 𝐴 × { 𝐵 } ) = { 𝐵 } )
8	5 7	eqtrd	⊢ ( 𝜑 → 𝐴 = { 𝐵 } )