Metamath Proof Explorer

Theorem pmtrdifellem2

Description: Lemma 2 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 pmtrdifellem2 ⊢ Q ∈ T → dom ⁡ S ∖ I = dom ⁡ Q ∖ I

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 3 difeq1i ⊢ S ∖ I = pmTrsp ⁡ N ⁡ dom ⁡ Q ∖ I ∖ I
5 4 dmeqi ⊢ dom ⁡ S ∖ I = dom ⁡ pmTrsp ⁡ N ⁡ dom ⁡ Q ∖ I ∖ I
6 eqid ⊢ pmTrsp ⁡ N ∖ K = pmTrsp ⁡ N ∖ K
7 6 1 pmtrfb ⊢ Q ∈ T ↔ N ∖ K ∈ V ∧ Q : N ∖ K ⟶ 1-1 onto N ∖ K ∧ dom ⁡ Q ∖ I ≈ 2 𝑜
8 difsnexi ⊢ N ∖ K ∈ V → N ∈ V
9 f1of ⊢ Q : N ∖ K ⟶ 1-1 onto N ∖ K → Q : N ∖ K ⟶ N ∖ K
10 fdm ⊢ Q : N ∖ K ⟶ N ∖ K → dom ⁡ Q = N ∖ K
11 difssd ⊢ dom ⁡ Q = N ∖ K → Q ∖ I ⊆ Q
12 dmss ⊢ Q ∖ I ⊆ Q → dom ⁡ Q ∖ I ⊆ dom ⁡ Q
13 11 12 syl ⊢ dom ⁡ Q = N ∖ K → dom ⁡ Q ∖ I ⊆ dom ⁡ Q
14 difssd ⊢ dom ⁡ Q = N ∖ K → N ∖ K ⊆ N
15 sseq1 ⊢ dom ⁡ Q = N ∖ K → dom ⁡ Q ⊆ N ↔ N ∖ K ⊆ N
16 14 15 mpbird ⊢ dom ⁡ Q = N ∖ K → dom ⁡ Q ⊆ N
17 13 16 sstrd ⊢ dom ⁡ Q = N ∖ K → dom ⁡ Q ∖ I ⊆ N
18 9 10 17 3syl ⊢ Q : N ∖ K ⟶ 1-1 onto N ∖ K → dom ⁡ Q ∖ I ⊆ N
19 id ⊢ dom ⁡ Q ∖ I ≈ 2 𝑜 → dom ⁡ Q ∖ I ≈ 2 𝑜
20 8 18 19 3anim123i ⊢ N ∖ K ∈ V ∧ Q : N ∖ K ⟶ 1-1 onto N ∖ K ∧ dom ⁡ Q ∖ I ≈ 2 𝑜 → N ∈ V ∧ dom ⁡ Q ∖ I ⊆ N ∧ dom ⁡ Q ∖ I ≈ 2 𝑜
21 7 20 sylbi ⊢ Q ∈ T → N ∈ V ∧ dom ⁡ Q ∖ I ⊆ N ∧ dom ⁡ Q ∖ I ≈ 2 𝑜
22 eqid ⊢ pmTrsp ⁡ N = pmTrsp ⁡ N
23 22 pmtrmvd ⊢ N ∈ V ∧ dom ⁡ Q ∖ I ⊆ N ∧ dom ⁡ Q ∖ I ≈ 2 𝑜 → dom ⁡ pmTrsp ⁡ N ⁡ dom ⁡ Q ∖ I ∖ I = dom ⁡ Q ∖ I
24 21 23 syl ⊢ Q ∈ T → dom ⁡ pmTrsp ⁡ N ⁡ dom ⁡ Q ∖ I ∖ I = dom ⁡ Q ∖ I
25 5 24 eqtrid ⊢ Q ∈ T → dom ⁡ S ∖ I = dom ⁡ Q ∖ I