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 ⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≈ 𝐵 )