isowe2

Description: A weak form of isowe that does not need Replacement. (Contributed by Mario Carneiro, 18-Nov-2014)

		Ref	Expression
	Assertion	isowe2	$⊢ (H {Isom}_{R, S} (A, B) \land \forall x H [x] \in V) \to (S We B \to R We A)$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (H {Isom}_{R, S} (A, B) \land \forall x H [x] \in V) \to H {Isom}_{R, S} (A, B)$
2		imaeq2	$⊢ x = y \to H [x] = H [y]$
3	2	eleq1d	$⊢ x = y \to (H [x] \in V \leftrightarrow H [y] \in V)$
4	3	spvv	$⊢ \forall x H [x] \in V \to H [y] \in V$
5	4	adantl	$⊢ (H {Isom}_{R, S} (A, B) \land \forall x H [x] \in V) \to H [y] \in V$
6	1 5	isofrlem	$⊢ (H {Isom}_{R, S} (A, B) \land \forall x H [x] \in V) \to (S Fr B \to R Fr A)$
7		isosolem	$⊢ H {Isom}_{R, S} (A, B) \to (S Or B \to R Or A)$
8	7	adantr	$⊢ (H {Isom}_{R, S} (A, B) \land \forall x H [x] \in V) \to (S Or B \to R Or A)$
9	6 8	anim12d	$⊢ (H {Isom}_{R, S} (A, B) \land \forall x H [x] \in V) \to ((S Fr B \land S Or B) \to (R Fr A \land R Or A))$
10		df-we	$⊢ S We B \leftrightarrow (S Fr B \land S Or B)$
11		df-we	$⊢ R We A \leftrightarrow (R Fr A \land R Or A)$
12	9 10 11	3imtr4g	$⊢ (H {Isom}_{R, S} (A, B) \land \forall x H [x] \in V) \to (S We B \to R We A)$

Metamath Proof Explorer