uptposlem

	Ref	Expression
Hypotheses	oppcuprcl2.x	No typesetting found for \|- ( ph -> X ( <. F , G >. ( O UP P ) W ) M ) with typecode \|-
	uptpos.h	$⊢ φ \to tpos G = H$
Assertion	uptposlem	$⊢ φ \to tpos H = G$

Step	Hyp	Ref	Expression
1		oppcuprcl2.x	Could not format ( ph -> X ( <. F , G >. ( O UP P ) W ) M ) : No typesetting found for \|- ( ph -> X ( <. F , G >. ( O UP P ) W ) M ) with typecode \|-
2		uptpos.h	$⊢ φ \to tpos G = H$
3	2	tposeqd	$⊢ φ \to tpos tpos G = tpos H$
4		eqid	$⊢ {Base}_{O} = {Base}_{O}$
5	1	uprcl2	$⊢ φ \to F (O Func P) G$
6	4 5	funcfn2	$⊢ φ \to G Fn ({Base}_{O} \times {Base}_{O})$
7		fnrel	$⊢ G Fn ({Base}_{O} \times {Base}_{O}) \to Rel G$
8	6 7	syl	$⊢ φ \to Rel G$
9		relxp	$⊢ Rel ({Base}_{O} \times {Base}_{O})$
10	6	fndmd	$⊢ φ \to dom G = {Base}_{O} \times {Base}_{O}$
11	10	releqd	$⊢ φ \to (Rel dom G \leftrightarrow Rel ({Base}_{O} \times {Base}_{O}))$
12	9 11	mpbiri	$⊢ φ \to Rel dom G$
13		tpostpos2	$⊢ (Rel G \land Rel dom G) \to tpos tpos G = G$
14	8 12 13	syl2anc	$⊢ φ \to tpos tpos G = G$
15	3 14	eqtr3d	$⊢ φ \to tpos H = G$

Metamath Proof Explorer