Metamath Proof Explorer

Theorem iscnrm3rlem1

Description: Lemma for iscnrm3rlem2 . The hypothesis could be generalized to ( ph -> ( S \ T ) C_ X ) . (Contributed by Zhi Wang, 5-Sep-2024)

Ref Expression
Hypothesis iscnrm3rlem1.1 
|- ( ph -> S C_ X )
Assertion iscnrm3rlem1 
|- ( ph -> ( S \ T ) = ( S i^i ( X \ ( S i^i T ) ) ) )

Proof

Step Hyp Ref Expression
1 iscnrm3rlem1.1 
 |-  ( ph -> S C_ X )
2 difindi 
 |-  ( X \ ( S i^i T ) ) = ( ( X \ S ) u. ( X \ T ) )
3 2 ineq2i 
 |-  ( S i^i ( X \ ( S i^i T ) ) ) = ( S i^i ( ( X \ S ) u. ( X \ T ) ) )
4 indi 
 |-  ( S i^i ( ( X \ S ) u. ( X \ T ) ) ) = ( ( S i^i ( X \ S ) ) u. ( S i^i ( X \ T ) ) )
5 disjdif 
 |-  ( S i^i ( X \ S ) ) = (/)
6 5 uneq1i 
 |-  ( ( S i^i ( X \ S ) ) u. ( S i^i ( X \ T ) ) ) = ( (/) u. ( S i^i ( X \ T ) ) )
7 0un 
 |-  ( (/) u. ( S i^i ( X \ T ) ) ) = ( S i^i ( X \ T ) )
8 indif2 
 |-  ( S i^i ( X \ T ) ) = ( ( S i^i X ) \ T )
9 6 7 8 3eqtri 
 |-  ( ( S i^i ( X \ S ) ) u. ( S i^i ( X \ T ) ) ) = ( ( S i^i X ) \ T )
10 3 4 9 3eqtri 
 |-  ( S i^i ( X \ ( S i^i T ) ) ) = ( ( S i^i X ) \ T )
11 df-ss 
 |-  ( S C_ X <-> ( S i^i X ) = S )
12 1 11 sylib 
 |-  ( ph -> ( S i^i X ) = S )
13 12 difeq1d 
 |-  ( ph -> ( ( S i^i X ) \ T ) = ( S \ T ) )
14 10 13 eqtr2id 
 |-  ( ph -> ( S \ T ) = ( S i^i ( X \ ( S i^i T ) ) ) )