sbthfilem

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

Metamath Proof Explorer

Theorem sbthfilem

Proof