Theorem sbthlem3

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

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

Proof

Step	Hyp	Ref	Expression
1		sbthlem.1	⊢ 𝐴 ∈ V
2		sbthlem.2	⊢ 𝐷 = { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝐴 ∖ 𝑥 ) ) }
3	1 2	sbthlem2	⊢ ( ran 𝑔 ⊆ 𝐴 → ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ⊆ ∪ 𝐷 )
4	1 2	sbthlem1	⊢ ∪ 𝐷 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) )
5	3 4	jctil	⊢ ( ran 𝑔 ⊆ 𝐴 → ( ∪ 𝐷 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ∧ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ⊆ ∪ 𝐷 ) )
6		eqss	⊢ ( ∪ 𝐷 = ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ↔ ( ∪ 𝐷 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ∧ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ⊆ ∪ 𝐷 ) )
7	5 6	sylibr	⊢ ( ran 𝑔 ⊆ 𝐴 → ∪ 𝐷 = ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) )
8	7	difeq2d	⊢ ( ran 𝑔 ⊆ 𝐴 → ( 𝐴 ∖ ∪ 𝐷 ) = ( 𝐴 ∖ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) )
9		imassrn	⊢ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ⊆ ran 𝑔
10		sstr2	⊢ ( ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ⊆ ran 𝑔 → ( ran 𝑔 ⊆ 𝐴 → ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ⊆ 𝐴 ) )
11	9 10	ax-mp	⊢ ( ran 𝑔 ⊆ 𝐴 → ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ⊆ 𝐴 )
12		dfss4	⊢ ( ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ⊆ 𝐴 ↔ ( 𝐴 ∖ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) = ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) )
13	11 12	sylib	⊢ ( ran 𝑔 ⊆ 𝐴 → ( 𝐴 ∖ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) = ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) )
14	8 13	eqtr2d	⊢ ( ran 𝑔 ⊆ 𝐴 → ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) = ( 𝐴 ∖ ∪ 𝐷 ) )