# Metamath Proof Explorer

## Theorem sbthlem10

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

Ref Expression
Hypotheses sbthlem.1 𝐴 ∈ V
sbthlem.2 𝐷 = { 𝑥 ∣ ( 𝑥𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ⊆ ( 𝐴𝑥 ) ) }
sbthlem.3 𝐻 = ( ( 𝑓 𝐷 ) ∪ ( 𝑔 ↾ ( 𝐴 𝐷 ) ) )
sbthlem.4 𝐵 ∈ V
Assertion sbthlem10 ( ( 𝐴𝐵𝐵𝐴 ) → 𝐴𝐵 )

### Proof

Step Hyp Ref Expression
1 sbthlem.1 𝐴 ∈ V
2 sbthlem.2 𝐷 = { 𝑥 ∣ ( 𝑥𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ⊆ ( 𝐴𝑥 ) ) }
3 sbthlem.3 𝐻 = ( ( 𝑓 𝐷 ) ∪ ( 𝑔 ↾ ( 𝐴 𝐷 ) ) )
4 sbthlem.4 𝐵 ∈ V
5 4 brdom ( 𝐴𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴1-1𝐵 )
6 1 brdom ( 𝐵𝐴 ↔ ∃ 𝑔 𝑔 : 𝐵1-1𝐴 )
7 5 6 anbi12i ( ( 𝐴𝐵𝐵𝐴 ) ↔ ( ∃ 𝑓 𝑓 : 𝐴1-1𝐵 ∧ ∃ 𝑔 𝑔 : 𝐵1-1𝐴 ) )
8 exdistrv ( ∃ 𝑓𝑔 ( 𝑓 : 𝐴1-1𝐵𝑔 : 𝐵1-1𝐴 ) ↔ ( ∃ 𝑓 𝑓 : 𝐴1-1𝐵 ∧ ∃ 𝑔 𝑔 : 𝐵1-1𝐴 ) )
9 7 8 bitr4i ( ( 𝐴𝐵𝐵𝐴 ) ↔ ∃ 𝑓𝑔 ( 𝑓 : 𝐴1-1𝐵𝑔 : 𝐵1-1𝐴 ) )
10 vex 𝑓 ∈ V
11 10 resex ( 𝑓 𝐷 ) ∈ V
12 vex 𝑔 ∈ V
13 12 cnvex 𝑔 ∈ V
14 13 resex ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ∈ V
15 11 14 unex ( ( 𝑓 𝐷 ) ∪ ( 𝑔 ↾ ( 𝐴 𝐷 ) ) ) ∈ V
16 3 15 eqeltri 𝐻 ∈ V
17 1 2 3 sbthlem9 ( ( 𝑓 : 𝐴1-1𝐵𝑔 : 𝐵1-1𝐴 ) → 𝐻 : 𝐴1-1-onto𝐵 )
18 f1oen3g ( ( 𝐻 ∈ V ∧ 𝐻 : 𝐴1-1-onto𝐵 ) → 𝐴𝐵 )
19 16 17 18 sylancr ( ( 𝑓 : 𝐴1-1𝐵𝑔 : 𝐵1-1𝐴 ) → 𝐴𝐵 )
20 19 exlimivv ( ∃ 𝑓𝑔 ( 𝑓 : 𝐴1-1𝐵𝑔 : 𝐵1-1𝐴 ) → 𝐴𝐵 )
21 9 20 sylbi ( ( 𝐴𝐵𝐵𝐴 ) → 𝐴𝐵 )