usgrexilem

Description: Lemma for usgrexi . (Contributed by AV, 12-Jan-2018) (Revised by AV, 10-Nov-2021)

		Ref	Expression
	Hypothesis	usgrexi.p	$⊢ P = \{x \in 𝒫 V \| \|x\| = 2\}$
	Assertion	usgrexilem	$⊢ V \in W \to ({I ↾}_{P}) : dom ({I ↾}_{P}) \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\}$

Step	Hyp	Ref	Expression
1		usgrexi.p	$⊢ P = \{x \in 𝒫 V \| \|x\| = 2\}$
2		f1oi	$⊢ ({I ↾}_{P}) : P \underset{1-1 onto}{⟶} P$
3		f1of1	$⊢ ({I ↾}_{P}) : P \underset{1-1 onto}{⟶} P \to ({I ↾}_{P}) : P \underset{1-1}{⟶} P$
4	2 3	ax-mp	$⊢ ({I ↾}_{P}) : P \underset{1-1}{⟶} P$
5		dmresi	$⊢ dom ({I ↾}_{P}) = P$
6		f1eq2	$⊢ dom ({I ↾}_{P}) = P \to (({I ↾}_{P}) : dom ({I ↾}_{P}) \underset{1-1}{⟶} P \leftrightarrow ({I ↾}_{P}) : P \underset{1-1}{⟶} P)$
7	5 6	ax-mp	$⊢ ({I ↾}_{P}) : dom ({I ↾}_{P}) \underset{1-1}{⟶} P \leftrightarrow ({I ↾}_{P}) : P \underset{1-1}{⟶} P$
8	4 7	mpbir	$⊢ ({I ↾}_{P}) : dom ({I ↾}_{P}) \underset{1-1}{⟶} P$
9	1	eqcomi	$⊢ \{x \in 𝒫 V \| \|x\| = 2\} = P$
10		f1eq3	$⊢ \{x \in 𝒫 V \| \|x\| = 2\} = P \to (({I ↾}_{P}) : dom ({I ↾}_{P}) \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\} \leftrightarrow ({I ↾}_{P}) : dom ({I ↾}_{P}) \underset{1-1}{⟶} P)$
11	9 10	mp1i	$⊢ V \in W \to (({I ↾}_{P}) : dom ({I ↾}_{P}) \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\} \leftrightarrow ({I ↾}_{P}) : dom ({I ↾}_{P}) \underset{1-1}{⟶} P)$
12	8 11	mpbiri	$⊢ V \in W \to ({I ↾}_{P}) : dom ({I ↾}_{P}) \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\}$

Metamath Proof Explorer