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 𝐻 = 𝐵 )