Theorem aks6d1c1p1rcl

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

	Ref	Expression
Hypotheses	aks6d1c1p1rcl.1	⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 𝐷 𝑦 ) ) ) }
	aks6d1c1p1rcl.2	⊢ ( 𝜑 → 𝐸 ∼ 𝐹 )
Assertion	aks6d1c1p1rcl	⊢ ( 𝜑 → ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		aks6d1c1p1rcl.1	⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 𝐷 𝑦 ) ) ) }
2		aks6d1c1p1rcl.2	⊢ ( 𝜑 → 𝐸 ∼ 𝐹 )
3		df-3an	⊢ ( ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 𝐷 𝑦 ) ) ) ↔ ( ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 𝐷 𝑦 ) ) ) )
4	3	opabbii	⊢ { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 𝐷 𝑦 ) ) ) } = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 𝐷 𝑦 ) ) ) }
5	1 4	eqtri	⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 𝐷 𝑦 ) ) ) }
6		opabssxp	⊢ { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 𝐷 𝑦 ) ) ) } ⊆ ( ℕ × 𝐵 )
7	5 6	eqsstri	⊢ ∼ ⊆ ( ℕ × 𝐵 )
8	7	brel	⊢ ( 𝐸 ∼ 𝐹 → ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ) )
9	2 8	syl	⊢ ( 𝜑 → ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ) )