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

Metamath Proof Explorer

Theorem sbthlem6

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

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

Proof

Step Hyp Ref Expression
1 sbthlem.1 ⊢ 𝐴 ∈ V
2 sbthlem.2 ⊢ 𝐷 = { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝐴 ∖ 𝑥 ) ) }
3 sbthlem.3 ⊢ 𝐻 = ( ( 𝑓 ↾ ∪ 𝐷 ) ∪ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) )
4 rnun ⊢ ran ( ( 𝑓 ↾ ∪ 𝐷 ) ∪ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) = ( ran ( 𝑓 ↾ ∪ 𝐷 ) ∪ ran ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) )
5 3 rneqi ⊢ ran 𝐻 = ran ( ( 𝑓 ↾ ∪ 𝐷 ) ∪ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) )
6 df-ima ⊢ ( 𝑓 “ ∪ 𝐷 ) = ran ( 𝑓 ↾ ∪ 𝐷 )
7 6 uneq1i ⊢ ( ( 𝑓 “ ∪ 𝐷 ) ∪ ran ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) = ( ran ( 𝑓 ↾ ∪ 𝐷 ) ∪ ran ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) )
8 4 5 7 3eqtr4i ⊢ ran 𝐻 = ( ( 𝑓 “ ∪ 𝐷 ) ∪ ran ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) )
9 1 2 sbthlem4 ⊢ ( ( ( dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) → ( ◡ 𝑔 “ ( 𝐴 ∖ ∪ 𝐷 ) ) = ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) )
10 df-ima ⊢ ( ◡ 𝑔 “ ( 𝐴 ∖ ∪ 𝐷 ) ) = ran ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) )
11 9 10 eqtr3di ⊢ ( ( ( dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) → ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) = ran ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) )
12 11 uneq2d ⊢ ( ( ( dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) → ( ( 𝑓 “ ∪ 𝐷 ) ∪ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) = ( ( 𝑓 “ ∪ 𝐷 ) ∪ ran ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) )
13 8 12 eqtr4id ⊢ ( ( ( dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) → ran 𝐻 = ( ( 𝑓 “ ∪ 𝐷 ) ∪ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) )
14 imassrn ⊢ ( 𝑓 “ ∪ 𝐷 ) ⊆ ran 𝑓
15 sstr2 ⊢ ( ( 𝑓 “ ∪ 𝐷 ) ⊆ ran 𝑓 → ( ran 𝑓 ⊆ 𝐵 → ( 𝑓 “ ∪ 𝐷 ) ⊆ 𝐵 ) )
16 14 15 ax-mp ⊢ ( ran 𝑓 ⊆ 𝐵 → ( 𝑓 “ ∪ 𝐷 ) ⊆ 𝐵 )
17 undif ⊢ ( ( 𝑓 “ ∪ 𝐷 ) ⊆ 𝐵 ↔ ( ( 𝑓 “ ∪ 𝐷 ) ∪ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) = 𝐵 )
18 16 17 sylib ⊢ ( ran 𝑓 ⊆ 𝐵 → ( ( 𝑓 “ ∪ 𝐷 ) ∪ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) = 𝐵 )
19 13 18 sylan9eqr ⊢ ( ( ran 𝑓 ⊆ 𝐵 ∧ ( ( dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → ran 𝐻 = 𝐵 )