This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbthlem4

Description: Lemma for sbth . (Contributed by NM, 27-Mar-1998)

Ref Expression
Hypotheses sbthlem.1 ⊢ 𝐴 ∈ V
sbthlem.2 ⊢ 𝐷 = { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝐴 ∖ 𝑥 ) ) }
Assertion sbthlem4 ( ( ( dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) → ( ◡ 𝑔 “ ( 𝐴 ∖ ∪ 𝐷 ) ) = ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 sbthlem.1 ⊢ 𝐴 ∈ V
2 sbthlem.2 ⊢ 𝐷 = { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝐴 ∖ 𝑥 ) ) }
3 df-ima ⊢ ( ◡ 𝑔 “ ( 𝐴 ∖ ∪ 𝐷 ) ) = ran ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) )
4 difss ⊢ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ⊆ 𝐵
5 sseq2 ⊢ ( dom 𝑔 = 𝐵 → ( ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ⊆ dom 𝑔 ↔ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ⊆ 𝐵 ) )
6 4 5 mpbiri ⊢ ( dom 𝑔 = 𝐵 → ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ⊆ dom 𝑔 )
7 ssdmres ⊢ ( ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ⊆ dom 𝑔 ↔ dom ( 𝑔 ↾ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) = ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) )
8 6 7 sylib ⊢ ( dom 𝑔 = 𝐵 → dom ( 𝑔 ↾ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) = ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) )
9 dfdm4 ⊢ dom ( 𝑔 ↾ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) = ran ◡ ( 𝑔 ↾ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) )
10 8 9 eqtr3di ⊢ ( dom 𝑔 = 𝐵 → ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) = ran ◡ ( 𝑔 ↾ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) )
11 funcnvres ⊢ ( Fun ◡ 𝑔 → ◡ ( 𝑔 ↾ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) = ( ◡ 𝑔 ↾ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) )
12 1 2 sbthlem3 ⊢ ( ran 𝑔 ⊆ 𝐴 → ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) = ( 𝐴 ∖ ∪ 𝐷 ) )
13 12 reseq2d ⊢ ( ran 𝑔 ⊆ 𝐴 → ( ◡ 𝑔 ↾ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) = ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) )
14 11 13 sylan9eqr ⊢ ( ( ran 𝑔 ⊆ 𝐴 ∧ Fun ◡ 𝑔 ) → ◡ ( 𝑔 ↾ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) = ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) )
15 14 rneqd ⊢ ( ( ran 𝑔 ⊆ 𝐴 ∧ Fun ◡ 𝑔 ) → ran ◡ ( 𝑔 ↾ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) = ran ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) )
16 10 15 sylan9eq ⊢ ( ( dom 𝑔 = 𝐵 ∧ ( ran 𝑔 ⊆ 𝐴 ∧ Fun ◡ 𝑔 ) ) → ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) = ran ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) )
17 16 anassrs ⊢ ( ( ( dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) → ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) = ran ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) )
18 3 17 eqtr4id ⊢ ( ( ( dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) → ( ◡ 𝑔 “ ( 𝐴 ∖ ∪ 𝐷 ) ) = ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) )