Metamath Proof Explorer

Theorem pmtrdifellem2

Description: Lemma 2 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 pmtrdifellem2 ( 𝑄 ∈ 𝑇 → dom ( 𝑆 ∖ I ) = dom ( 𝑄 ∖ I ) )

Proof

Step Hyp Ref Expression
1 pmtrdifel.t ⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
2 pmtrdifel.r ⊢ 𝑅 = ran ( pmTrsp ‘ 𝑁 )
3 pmtrdifel.0 ⊢ 𝑆 = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑄 ∖ I ) )
4 3 difeq1i ⊢ ( 𝑆 ∖ I ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑄 ∖ I ) ) ∖ I )
5 4 dmeqi ⊢ dom ( 𝑆 ∖ I ) = dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑄 ∖ I ) ) ∖ I )
6 eqid ⊢ ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) = ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
7 6 1 pmtrfb ⊢ ( 𝑄 ∈ 𝑇 ↔ ( ( 𝑁 ∖ { 𝐾 } ) ∈ V ∧ 𝑄 : ( 𝑁 ∖ { 𝐾 } ) –1-1-onto→ ( 𝑁 ∖ { 𝐾 } ) ∧ dom ( 𝑄 ∖ I ) ≈ 2o ) )
8 difsnexi ⊢ ( ( 𝑁 ∖ { 𝐾 } ) ∈ V → 𝑁 ∈ V )
9 f1of ⊢ ( 𝑄 : ( 𝑁 ∖ { 𝐾 } ) –1-1-onto→ ( 𝑁 ∖ { 𝐾 } ) → 𝑄 : ( 𝑁 ∖ { 𝐾 } ) ⟶ ( 𝑁 ∖ { 𝐾 } ) )
10 fdm ⊢ ( 𝑄 : ( 𝑁 ∖ { 𝐾 } ) ⟶ ( 𝑁 ∖ { 𝐾 } ) → dom 𝑄 = ( 𝑁 ∖ { 𝐾 } ) )
11 difssd ⊢ ( dom 𝑄 = ( 𝑁 ∖ { 𝐾 } ) → ( 𝑄 ∖ I ) ⊆ 𝑄 )
12 dmss ⊢ ( ( 𝑄 ∖ I ) ⊆ 𝑄 → dom ( 𝑄 ∖ I ) ⊆ dom 𝑄 )
13 11 12 syl ⊢ ( dom 𝑄 = ( 𝑁 ∖ { 𝐾 } ) → dom ( 𝑄 ∖ I ) ⊆ dom 𝑄 )
14 difssd ⊢ ( dom 𝑄 = ( 𝑁 ∖ { 𝐾 } ) → ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 )
15 sseq1 ⊢ ( dom 𝑄 = ( 𝑁 ∖ { 𝐾 } ) → ( dom 𝑄 ⊆ 𝑁 ↔ ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 ) )
16 14 15 mpbird ⊢ ( dom 𝑄 = ( 𝑁 ∖ { 𝐾 } ) → dom 𝑄 ⊆ 𝑁 )
17 13 16 sstrd ⊢ ( dom 𝑄 = ( 𝑁 ∖ { 𝐾 } ) → dom ( 𝑄 ∖ I ) ⊆ 𝑁 )
18 9 10 17 3syl ⊢ ( 𝑄 : ( 𝑁 ∖ { 𝐾 } ) –1-1-onto→ ( 𝑁 ∖ { 𝐾 } ) → dom ( 𝑄 ∖ I ) ⊆ 𝑁 )
19 id ⊢ ( dom ( 𝑄 ∖ I ) ≈ 2o → dom ( 𝑄 ∖ I ) ≈ 2o )
20 8 18 19 3anim123i ⊢ ( ( ( 𝑁 ∖ { 𝐾 } ) ∈ V ∧ 𝑄 : ( 𝑁 ∖ { 𝐾 } ) –1-1-onto→ ( 𝑁 ∖ { 𝐾 } ) ∧ dom ( 𝑄 ∖ I ) ≈ 2o ) → ( 𝑁 ∈ V ∧ dom ( 𝑄 ∖ I ) ⊆ 𝑁 ∧ dom ( 𝑄 ∖ I ) ≈ 2o ) )
21 7 20 sylbi ⊢ ( 𝑄 ∈ 𝑇 → ( 𝑁 ∈ V ∧ dom ( 𝑄 ∖ I ) ⊆ 𝑁 ∧ dom ( 𝑄 ∖ I ) ≈ 2o ) )
22 eqid ⊢ ( pmTrsp ‘ 𝑁 ) = ( pmTrsp ‘ 𝑁 )
23 22 pmtrmvd ⊢ ( ( 𝑁 ∈ V ∧ dom ( 𝑄 ∖ I ) ⊆ 𝑁 ∧ dom ( 𝑄 ∖ I ) ≈ 2o ) → dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑄 ∖ I ) ) ∖ I ) = dom ( 𝑄 ∖ I ) )
24 21 23 syl ⊢ ( 𝑄 ∈ 𝑇 → dom ( ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑄 ∖ I ) ) ∖ I ) = dom ( 𝑄 ∖ I ) )
25 5 24 syl5eq ⊢ ( 𝑄 ∈ 𝑇 → dom ( 𝑆 ∖ I ) = dom ( 𝑄 ∖ I ) )