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 ◡ 𝑔 ) → ( ◡ 𝑔 “ ( 𝐴 ∖ ∪ 𝐷 ) ) = ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) )