Metamath Proof Explorer

Theorem psrbagleclOLD

Description: Obsolete version of psrbaglecl as of 5-Aug-2024. (Contributed by Mario Carneiro, 29-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	Assertion	psrbagleclOLD	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to G \in D$

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
2		simpr2	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to G : I ⟶ ℕ_{0}$
3		simpr1	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to F \in D$
4	1	psrbag	$⊢ I \in V \to (F \in D \leftrightarrow (F : I ⟶ ℕ_{0} \land F^{-1} [ℕ] \in Fin))$
5	4	adantr	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to (F \in D \leftrightarrow (F : I ⟶ ℕ_{0} \land F^{-1} [ℕ] \in Fin))$
6	3 5	mpbid	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to (F : I ⟶ ℕ_{0} \land F^{-1} [ℕ] \in Fin)$
7	6	simprd	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to F^{-1} [ℕ] \in Fin$
8	1	psrbaglesuppOLD	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to G^{-1} [ℕ] \subseteq F^{-1} [ℕ]$
9	7 8	ssfid	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to G^{-1} [ℕ] \in Fin$
10	1	psrbag	$⊢ I \in V \to (G \in D \leftrightarrow (G : I ⟶ ℕ_{0} \land G^{-1} [ℕ] \in Fin))$
11	10	adantr	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to (G \in D \leftrightarrow (G : I ⟶ ℕ_{0} \land G^{-1} [ℕ] \in Fin))$
12	2 9 11	mpbir2and	$⊢ (I \in V \land (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F)) \to G \in D$