Metamath Proof Explorer

Theorem kardexOLD

Description: Obsolete version of kardex as of 19-Jul-2026. (Contributed by NM, 14-Dec-2003) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion kardexOLD ⊢ x | x ≈ A ∧ ∀ y y ≈ A → rank ⁡ x ⊆ rank ⁡ y ∈ V

Proof

Step Hyp Ref Expression
1 df-rab ⊢ x ∈ z | z ≈ A | ∀ y ∈ z | z ≈ A rank ⁡ x ⊆ rank ⁡ y = x | x ∈ z | z ≈ A ∧ ∀ y ∈ z | z ≈ A rank ⁡ x ⊆ rank ⁡ y
2 vex ⊢ x ∈ V
3 breq1 ⊢ z = x → z ≈ A ↔ x ≈ A
4 2 3 elab ⊢ x ∈ z | z ≈ A ↔ x ≈ A
5 breq1 ⊢ z = y → z ≈ A ↔ y ≈ A
6 5 ralab ⊢ ∀ y ∈ z | z ≈ A rank ⁡ x ⊆ rank ⁡ y ↔ ∀ y y ≈ A → rank ⁡ x ⊆ rank ⁡ y
7 4 6 anbi12i ⊢ x ∈ z | z ≈ A ∧ ∀ y ∈ z | z ≈ A rank ⁡ x ⊆ rank ⁡ y ↔ x ≈ A ∧ ∀ y y ≈ A → rank ⁡ x ⊆ rank ⁡ y
8 7 abbii ⊢ x | x ∈ z | z ≈ A ∧ ∀ y ∈ z | z ≈ A rank ⁡ x ⊆ rank ⁡ y = x | x ≈ A ∧ ∀ y y ≈ A → rank ⁡ x ⊆ rank ⁡ y
9 1 8 eqtri ⊢ x ∈ z | z ≈ A | ∀ y ∈ z | z ≈ A rank ⁡ x ⊆ rank ⁡ y = x | x ≈ A ∧ ∀ y y ≈ A → rank ⁡ x ⊆ rank ⁡ y
10 scottexOLD ⊢ x ∈ z | z ≈ A | ∀ y ∈ z | z ≈ A rank ⁡ x ⊆ rank ⁡ y ∈ V
11 9 10 eqeltrri ⊢ x | x ≈ A ∧ ∀ y y ≈ A → rank ⁡ x ⊆ rank ⁡ y ∈ V