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 ∈ T → ∀ x ∈ 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 ∈ T → dom ⁡ S ∖ I = dom ⁡ Q ∖ I
5 4 adantr ⊢ Q ∈ T ∧ x ∈ N ∖ K → dom ⁡ S ∖ I = dom ⁡ Q ∖ I
6 5 eleq2d ⊢ Q ∈ T ∧ x ∈ N ∖ K → x ∈ dom ⁡ S ∖ I ↔ x ∈ dom ⁡ Q ∖ I
7 4 difeq1d ⊢ Q ∈ T → dom ⁡ S ∖ I ∖ x = dom ⁡ Q ∖ I ∖ x
8 7 unieqd ⊢ Q ∈ T → ⋃ dom ⁡ S ∖ I ∖ x = ⋃ dom ⁡ Q ∖ I ∖ x
9 8 adantr ⊢ Q ∈ T ∧ x ∈ N ∖ K → ⋃ dom ⁡ S ∖ I ∖ x = ⋃ dom ⁡ Q ∖ I ∖ x
10 6 9 ifbieq1d ⊢ Q ∈ T ∧ x ∈ N ∖ K → if x ∈ dom ⁡ S ∖ I ⋃ dom ⁡ S ∖ I ∖ x x = if x ∈ dom ⁡ Q ∖ I ⋃ dom ⁡ Q ∖ I ∖ x x
11 1 2 3 pmtrdifellem1 ⊢ Q ∈ T → S ∈ R
12 eldifi ⊢ x ∈ N ∖ K → x ∈ N
13 eqid ⊢ pmTrsp ⁡ N = pmTrsp ⁡ N
14 eqid ⊢ dom ⁡ S ∖ I = dom ⁡ S ∖ I
15 13 2 14 pmtrffv ⊢ S ∈ R ∧ x ∈ N → S ⁡ x = if x ∈ dom ⁡ S ∖ I ⋃ dom ⁡ S ∖ I ∖ x x
16 11 12 15 syl2an ⊢ Q ∈ T ∧ x ∈ N ∖ K → S ⁡ x = if x ∈ dom ⁡ S ∖ I ⋃ 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 ∈ T ∧ x ∈ N ∖ K → Q ⁡ x = if x ∈ dom ⁡ Q ∖ I ⋃ dom ⁡ Q ∖ I ∖ x x
20 10 16 19 3eqtr4rd ⊢ Q ∈ T ∧ x ∈ N ∖ K → Q ⁡ x = S ⁡ x
21 20 ralrimiva ⊢ Q ∈ T → ∀ x ∈ N ∖ K Q ⁡ x = S ⁡ x