Metamath Proof Explorer

Theorem aks6d1c1p1rcl

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

Ref Expression
Hypotheses aks6d1c1p1rcl.1 ⊢ ∼ ˙ = e f | e ∈ ℕ ∧ f ∈ B ∧ ∀ y ∈ K PrimRoots R e × ˙ O ⁡ f ⁡ y = O ⁡ f ⁡ e D y
aks6d1c1p1rcl.2 ⊢ φ → E ∼ ˙ F
Assertion aks6d1c1p1rcl ⊢ φ → E ∈ ℕ ∧ F ∈ B

Proof

Step Hyp Ref Expression
1 aks6d1c1p1rcl.1 ⊢ ∼ ˙ = e f | e ∈ ℕ ∧ f ∈ B ∧ ∀ y ∈ K PrimRoots R e × ˙ O ⁡ f ⁡ y = O ⁡ f ⁡ e D y
2 aks6d1c1p1rcl.2 ⊢ φ → E ∼ ˙ F
3 df-3an ⊢ e ∈ ℕ ∧ f ∈ B ∧ ∀ y ∈ K PrimRoots R e × ˙ O ⁡ f ⁡ y = O ⁡ f ⁡ e D y ↔ e ∈ ℕ ∧ f ∈ B ∧ ∀ y ∈ K PrimRoots R e × ˙ O ⁡ f ⁡ y = O ⁡ f ⁡ e D y
4 3 opabbii ⊢ e f | e ∈ ℕ ∧ f ∈ B ∧ ∀ y ∈ K PrimRoots R e × ˙ O ⁡ f ⁡ y = O ⁡ f ⁡ e D y = e f | e ∈ ℕ ∧ f ∈ B ∧ ∀ y ∈ K PrimRoots R e × ˙ O ⁡ f ⁡ y = O ⁡ f ⁡ e D y
5 1 4 eqtri ⊢ ∼ ˙ = e f | e ∈ ℕ ∧ f ∈ B ∧ ∀ y ∈ K PrimRoots R e × ˙ O ⁡ f ⁡ y = O ⁡ f ⁡ e D y
6 opabssxp ⊢ e f | e ∈ ℕ ∧ f ∈ B ∧ ∀ y ∈ K PrimRoots R e × ˙ O ⁡ f ⁡ y = O ⁡ f ⁡ e D y ⊆ ℕ × B
7 5 6 eqsstri ⊢ ∼ ˙ ⊆ ℕ × B
8 7 brel ⊢ E ∼ ˙ F → E ∈ ℕ ∧ F ∈ B
9 2 8 syl ⊢ φ → E ∈ ℕ ∧ F ∈ B