Theorem aks6d1c1p1rcl

Description: Reverse closure of the introspective relation. (Contributed by metakunt, 25-Apr-2025)

	Ref	Expression
Hypotheses	aks6d1c1p1rcl.1	|- .~ = { <. e , f >. | ( e e. NN /\ f e. B /\ A. y e. ( K PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e D y ) ) ) }
	aks6d1c1p1rcl.2	|- ( ph -> E .~ F )
Assertion	aks6d1c1p1rcl	|- ( ph -> ( E e. NN /\ F e. B ) )

Proof

Step	Hyp	Ref	Expression
1		aks6d1c1p1rcl.1	|- .~ = { <. e , f >. | ( e e. NN /\ f e. B /\ A. y e. ( K PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e D y ) ) ) }
2		aks6d1c1p1rcl.2	|- ( ph -> E .~ F )
3		df-3an	|- ( ( e e. NN /\ f e. B /\ A. y e. ( K PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e D y ) ) ) <-> ( ( e e. NN /\ f e. B ) /\ A. y e. ( K PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e D y ) ) ) )
4	3	opabbii	|- { <. e , f >. | ( e e. NN /\ f e. B /\ A. y e. ( K PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e D y ) ) ) } = { <. e , f >. | ( ( e e. NN /\ f e. B ) /\ A. y e. ( K PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e D y ) ) ) }
5	1 4	eqtri	|- .~ = { <. e , f >. | ( ( e e. NN /\ f e. B ) /\ A. y e. ( K PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e D y ) ) ) }
6		opabssxp	|- { <. e , f >. | ( ( e e. NN /\ f e. B ) /\ A. y e. ( K PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e D y ) ) ) } C_ ( NN X. B )
7	5 6	eqsstri	|- .~ C_ ( NN X. B )
8	7	brel	|- ( E .~ F -> ( E e. NN /\ F e. B ) )
9	2 8	syl	|- ( ph -> ( E e. NN /\ F e. B ) )