Theorem pmtrdifellem3

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

	Ref	Expression
Hypotheses	pmtrdifel.t	⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
	pmtrdifel.r	⊢ 𝑅 = ran ( pmTrsp ‘ 𝑁 )
	pmtrdifel.0	⊢ 𝑆 = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑄 ∖ I ) )
Assertion	pmtrdifellem3	⊢ ( 𝑄 ∈ 𝑇 → ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑄 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		pmtrdifel.t	⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
2		pmtrdifel.r	⊢ 𝑅 = ran ( pmTrsp ‘ 𝑁 )
3		pmtrdifel.0	⊢ 𝑆 = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑄 ∖ I ) )
4	1 2 3	pmtrdifellem2	⊢ ( 𝑄 ∈ 𝑇 → dom ( 𝑆 ∖ I ) = dom ( 𝑄 ∖ I ) )
5	4	adantr	⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → dom ( 𝑆 ∖ I ) = dom ( 𝑄 ∖ I ) )
6	5	eleq2d	⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑥 ∈ dom ( 𝑆 ∖ I ) ↔ 𝑥 ∈ dom ( 𝑄 ∖ I ) ) )
7	4	difeq1d	⊢ ( 𝑄 ∈ 𝑇 → ( dom ( 𝑆 ∖ I ) ∖ { 𝑥 } ) = ( dom ( 𝑄 ∖ I ) ∖ { 𝑥 } ) )
8	7	unieqd	⊢ ( 𝑄 ∈ 𝑇 → ∪ ( dom ( 𝑆 ∖ I ) ∖ { 𝑥 } ) = ∪ ( dom ( 𝑄 ∖ I ) ∖ { 𝑥 } ) )
9	8	adantr	⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ∪ ( dom ( 𝑆 ∖ I ) ∖ { 𝑥 } ) = ∪ ( dom ( 𝑄 ∖ I ) ∖ { 𝑥 } ) )
10	6 9	ifbieq1d	⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → if ( 𝑥 ∈ dom ( 𝑆 ∖ I ) , ∪ ( dom ( 𝑆 ∖ I ) ∖ { 𝑥 } ) , 𝑥 ) = if ( 𝑥 ∈ dom ( 𝑄 ∖ I ) , ∪ ( dom ( 𝑄 ∖ I ) ∖ { 𝑥 } ) , 𝑥 ) )
11	1 2 3	pmtrdifellem1	⊢ ( 𝑄 ∈ 𝑇 → 𝑆 ∈ 𝑅 )
12		eldifi	⊢ ( 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) → 𝑥 ∈ 𝑁 )
13		eqid	⊢ ( pmTrsp ‘ 𝑁 ) = ( pmTrsp ‘ 𝑁 )
14		eqid	⊢ dom ( 𝑆 ∖ I ) = dom ( 𝑆 ∖ I )
15	13 2 14	pmtrffv	⊢ ( ( 𝑆 ∈ 𝑅 ∧ 𝑥 ∈ 𝑁 ) → ( 𝑆 ‘ 𝑥 ) = if ( 𝑥 ∈ dom ( 𝑆 ∖ I ) , ∪ ( dom ( 𝑆 ∖ I ) ∖ { 𝑥 } ) , 𝑥 ) )
16	11 12 15	syl2an	⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑆 ‘ 𝑥 ) = if ( 𝑥 ∈ dom ( 𝑆 ∖ I ) , ∪ ( dom ( 𝑆 ∖ I ) ∖ { 𝑥 } ) , 𝑥 ) )
17		eqid	⊢ ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) = ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
18		eqid	⊢ dom ( 𝑄 ∖ I ) = dom ( 𝑄 ∖ I )
19	17 1 18	pmtrffv	⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑄 ‘ 𝑥 ) = if ( 𝑥 ∈ dom ( 𝑄 ∖ I ) , ∪ ( dom ( 𝑄 ∖ I ) ∖ { 𝑥 } ) , 𝑥 ) )
20	10 16 19	3eqtr4rd	⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑄 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
21	20	ralrimiva	⊢ ( 𝑄 ∈ 𝑇 → ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑄 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )