This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbthfilem

Description: Lemma for sbthfi . (Contributed by BTernaryTau, 4-Nov-2024)

Ref Expression
Hypotheses sbthfilem.1 ⊢ 𝐴 ∈ V
sbthfilem.2 ⊢ 𝐷 = { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝐴 ∖ 𝑥 ) ) }
sbthfilem.3 ⊢ 𝐻 = ( ( 𝑓 ↾ ∪ 𝐷 ) ∪ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) )
sbthfilem.4 ⊢ 𝐵 ∈ V
Assertion sbthfilem ( ( 𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≈ 𝐵 )

Proof

Step Hyp Ref Expression
1 sbthfilem.1 ⊢ 𝐴 ∈ V
2 sbthfilem.2 ⊢ 𝐷 = { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝐴 ∖ 𝑥 ) ) }
3 sbthfilem.3 ⊢ 𝐻 = ( ( 𝑓 ↾ ∪ 𝐷 ) ∪ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) )
4 sbthfilem.4 ⊢ 𝐵 ∈ V
5 19.42vv ⊢ ( ∃ 𝑓 ∃ 𝑔 ( 𝐵 ∈ Fin ∧ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) ) ↔ ( 𝐵 ∈ Fin ∧ ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) ) )
6 3anass ⊢ ( ( 𝐵 ∈ Fin ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) ↔ ( 𝐵 ∈ Fin ∧ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) ) )
7 6 2exbii ⊢ ( ∃ 𝑓 ∃ 𝑔 ( 𝐵 ∈ Fin ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) ↔ ∃ 𝑓 ∃ 𝑔 ( 𝐵 ∈ Fin ∧ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) ) )
8 3anass ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) ↔ ( 𝐵 ∈ Fin ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) ) )
9 4 brdom ⊢ ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 )
10 1 brdom ⊢ ( 𝐵 ≼ 𝐴 ↔ ∃ 𝑔 𝑔 : 𝐵 –1-1→ 𝐴 )
11 9 10 anbi12i ⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) ↔ ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ∧ ∃ 𝑔 𝑔 : 𝐵 –1-1→ 𝐴 ) )
12 exdistrv ⊢ ( ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) ↔ ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ∧ ∃ 𝑔 𝑔 : 𝐵 –1-1→ 𝐴 ) )
13 11 12 bitr4i ⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) ↔ ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) )
14 13 anbi2i ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) ) ↔ ( 𝐵 ∈ Fin ∧ ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) ) )
15 8 14 bitri ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) ↔ ( 𝐵 ∈ Fin ∧ ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) ) )
16 5 7 15 3bitr4ri ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) ↔ ∃ 𝑓 ∃ 𝑔 ( 𝐵 ∈ Fin ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) )
17 f1fn ⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 → 𝑔 Fn 𝐵 )
18 vex ⊢ 𝑓 ∈ V
19 18 resex ⊢ ( 𝑓 ↾ ∪ 𝐷 ) ∈ V
20 fnfi ⊢ ( ( 𝑔 Fn 𝐵 ∧ 𝐵 ∈ Fin ) → 𝑔 ∈ Fin )
21 cnvfi ⊢ ( 𝑔 ∈ Fin → ◡ 𝑔 ∈ Fin )
22 resexg ⊢ ( ◡ 𝑔 ∈ Fin → ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ∈ V )
23 20 21 22 3syl ⊢ ( ( 𝑔 Fn 𝐵 ∧ 𝐵 ∈ Fin ) → ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ∈ V )
24 unexg ⊢ ( ( ( 𝑓 ↾ ∪ 𝐷 ) ∈ V ∧ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ∈ V ) → ( ( 𝑓 ↾ ∪ 𝐷 ) ∪ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) ∈ V )
25 19 23 24 sylancr ⊢ ( ( 𝑔 Fn 𝐵 ∧ 𝐵 ∈ Fin ) → ( ( 𝑓 ↾ ∪ 𝐷 ) ∪ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) ∈ V )
26 3 25 eqeltrid ⊢ ( ( 𝑔 Fn 𝐵 ∧ 𝐵 ∈ Fin ) → 𝐻 ∈ V )
27 26 ancoms ⊢ ( ( 𝐵 ∈ Fin ∧ 𝑔 Fn 𝐵 ) → 𝐻 ∈ V )
28 17 27 sylan2 ⊢ ( ( 𝐵 ∈ Fin ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) → 𝐻 ∈ V )
29 28 3adant2 ⊢ ( ( 𝐵 ∈ Fin ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) → 𝐻 ∈ V )
30 1 2 3 sbthlem9 ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 )
31 30 3adant1 ⊢ ( ( 𝐵 ∈ Fin ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 )
32 f1oen3g ⊢ ( ( 𝐻 ∈ V ∧ 𝐻 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐴 ≈ 𝐵 )
33 29 31 32 syl2anc ⊢ ( ( 𝐵 ∈ Fin ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) → 𝐴 ≈ 𝐵 )
34 33 exlimivv ⊢ ( ∃ 𝑓 ∃ 𝑔 ( 𝐵 ∈ Fin ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) → 𝐴 ≈ 𝐵 )
35 16 34 sylbi ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≈ 𝐵 )