Metamath Proof Explorer

Theorem pmtrdifellem3

Description: Lemma 3 for pmtrdifel . (Contributed by AV, 15-Jan-2019)

Ref Expression
Hypotheses pmtrdifel.t 
|- T = ran ( pmTrsp ` ( N \ { K } ) )
pmtrdifel.r 
|- R = ran ( pmTrsp ` N )
pmtrdifel.0 
|- S = ( ( pmTrsp ` N ) ` dom ( Q \ _I ) )
Assertion pmtrdifellem3 
|- ( Q e. T -> A. x e. ( N \ { K } ) ( Q ` x ) = ( S ` x ) )

Proof

Step Hyp Ref Expression
1 pmtrdifel.t 
 |-  T = ran ( pmTrsp ` ( N \ { K } ) )
2 pmtrdifel.r 
 |-  R = ran ( pmTrsp ` N )
3 pmtrdifel.0 
 |-  S = ( ( pmTrsp ` N ) ` dom ( Q \ _I ) )
4 1 2 3 pmtrdifellem2 
 |-  ( Q e. T -> dom ( S \ _I ) = dom ( Q \ _I ) )
5 4 adantr 
 |-  ( ( Q e. T /\ x e. ( N \ { K } ) ) -> dom ( S \ _I ) = dom ( Q \ _I ) )
6 5 eleq2d 
 |-  ( ( Q e. T /\ x e. ( N \ { K } ) ) -> ( x e. dom ( S \ _I ) <-> x e. dom ( Q \ _I ) ) )
7 4 difeq1d 
 |-  ( Q e. T -> ( dom ( S \ _I ) \ { x } ) = ( dom ( Q \ _I ) \ { x } ) )
8 7 unieqd 
 |-  ( Q e. T -> U. ( dom ( S \ _I ) \ { x } ) = U. ( dom ( Q \ _I ) \ { x } ) )
9 8 adantr 
 |-  ( ( Q e. T /\ x e. ( N \ { K } ) ) -> U. ( dom ( S \ _I ) \ { x } ) = U. ( dom ( Q \ _I ) \ { x } ) )
10 6 9 ifbieq1d 
 |-  ( ( Q e. T /\ x e. ( N \ { K } ) ) -> if ( x e. dom ( S \ _I ) , U. ( dom ( S \ _I ) \ { x } ) , x ) = if ( x e. dom ( Q \ _I ) , U. ( dom ( Q \ _I ) \ { x } ) , x ) )
11 1 2 3 pmtrdifellem1 
 |-  ( Q e. T -> S e. R )
12 eldifi 
 |-  ( x e. ( N \ { K } ) -> x e. N )
13 eqid 
 |-  ( pmTrsp ` N ) = ( pmTrsp ` N )
14 eqid 
 |-  dom ( S \ _I ) = dom ( S \ _I )
15 13 2 14 pmtrffv 
 |-  ( ( S e. R /\ x e. N ) -> ( S ` x ) = if ( x e. dom ( S \ _I ) , U. ( dom ( S \ _I ) \ { x } ) , x ) )
16 11 12 15 syl2an 
 |-  ( ( Q e. T /\ x e. ( N \ { K } ) ) -> ( S ` x ) = if ( x e. dom ( S \ _I ) , U. ( dom ( S \ _I ) \ { x } ) , x ) )
17 eqid 
 |-  ( pmTrsp ` ( N \ { K } ) ) = ( pmTrsp ` ( N \ { K } ) )
18 eqid 
 |-  dom ( Q \ _I ) = dom ( Q \ _I )
19 17 1 18 pmtrffv 
 |-  ( ( Q e. T /\ x e. ( N \ { K } ) ) -> ( Q ` x ) = if ( x e. dom ( Q \ _I ) , U. ( dom ( Q \ _I ) \ { x } ) , x ) )
20 10 16 19 3eqtr4rd 
 |-  ( ( Q e. T /\ x e. ( N \ { K } ) ) -> ( Q ` x ) = ( S ` x ) )
21 20 ralrimiva 
 |-  ( Q e. T -> A. x e. ( N \ { K } ) ( Q ` x ) = ( S ` x ) )