Metamath Proof Explorer

Theorem entrfil

Description: Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr ). (Contributed by BTernaryTau, 10-Sep-2024)

		Ref	Expression
	Assertion	entrfil	$⊢ (A \in Fin \land A \approx B \land B \approx C) \to A \approx C$

Proof

Step	Hyp	Ref	Expression
1		bren	$⊢ B \approx C \leftrightarrow \exists f f : B \underset{1-1 onto}{⟶} C$
2		bren	$⊢ A \approx B \leftrightarrow \exists g g : A \underset{1-1 onto}{⟶} B$
3		exdistrv	$⊢ \exists g \exists f (g : A \underset{1-1 onto}{⟶} B \land f : B \underset{1-1 onto}{⟶} C) \leftrightarrow (\exists g g : A \underset{1-1 onto}{⟶} B \land \exists f f : B \underset{1-1 onto}{⟶} C)$
4		19.42vv	$⊢ \exists g \exists f (A \in Fin \land (g : A \underset{1-1 onto}{⟶} B \land f : B \underset{1-1 onto}{⟶} C)) \leftrightarrow (A \in Fin \land \exists g \exists f (g : A \underset{1-1 onto}{⟶} B \land f : B \underset{1-1 onto}{⟶} C))$
5		f1oco	$⊢ (f : B \underset{1-1 onto}{⟶} C \land g : A \underset{1-1 onto}{⟶} B) \to (f \circ g) : A \underset{1-1 onto}{⟶} C$
6	5	ancoms	$⊢ (g : A \underset{1-1 onto}{⟶} B \land f : B \underset{1-1 onto}{⟶} C) \to (f \circ g) : A \underset{1-1 onto}{⟶} C$
7		f1oenfi	$⊢ (A \in Fin \land (f \circ g) : A \underset{1-1 onto}{⟶} C) \to A \approx C$
8	6 7	sylan2	$⊢ (A \in Fin \land (g : A \underset{1-1 onto}{⟶} B \land f : B \underset{1-1 onto}{⟶} C)) \to A \approx C$
9	8	exlimivv	$⊢ \exists g \exists f (A \in Fin \land (g : A \underset{1-1 onto}{⟶} B \land f : B \underset{1-1 onto}{⟶} C)) \to A \approx C$
10	4 9	sylbir	$⊢ (A \in Fin \land \exists g \exists f (g : A \underset{1-1 onto}{⟶} B \land f : B \underset{1-1 onto}{⟶} C)) \to A \approx C$
11	3 10	sylan2br	$⊢ (A \in Fin \land (\exists g g : A \underset{1-1 onto}{⟶} B \land \exists f f : B \underset{1-1 onto}{⟶} C)) \to A \approx C$
12	11	3impb	$⊢ (A \in Fin \land \exists g g : A \underset{1-1 onto}{⟶} B \land \exists f f : B \underset{1-1 onto}{⟶} C) \to A \approx C$
13	2 12	syl3an2b	$⊢ (A \in Fin \land A \approx B \land \exists f f : B \underset{1-1 onto}{⟶} C) \to A \approx C$
14	1 13	syl3an3b	$⊢ (A \in Fin \land A \approx B \land B \approx C) \to A \approx C$