Metamath Proof Explorer

Theorem dfdfat2

Description: Alternate definition of the predicate "defined at" not using the Fun predicate. (Contributed by Alexander van der Vekens, 22-Jul-2017) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion dfdfat2 ⊢ F defAt A ↔ A ∈ dom ⁡ F ∧ ∃! y A F y

Proof

Step Hyp Ref Expression
1 df-dfat ⊢ F defAt A ↔ A ∈ dom ⁡ F ∧ Fun ⁡ F ↾ A
2 relres ⊢ Rel ⁡ F ↾ A
3 dffun8 ⊢ Fun ⁡ F ↾ A ↔ Rel ⁡ F ↾ A ∧ ∀ x ∈ dom ⁡ F ↾ A ∃! y x F ↾ A y
4 2 3 mpbiran ⊢ Fun ⁡ F ↾ A ↔ ∀ x ∈ dom ⁡ F ↾ A ∃! y x F ↾ A y
5 4 anbi2i ⊢ A ∈ dom ⁡ F ∧ Fun ⁡ F ↾ A ↔ A ∈ dom ⁡ F ∧ ∀ x ∈ dom ⁡ F ↾ A ∃! y x F ↾ A y
6 brres ⊢ y ∈ V → x F ↾ A y ↔ x ∈ A ∧ x F y
7 6 elv ⊢ x F ↾ A y ↔ x ∈ A ∧ x F y
8 7 a1i ⊢ A ∈ dom ⁡ F → x F ↾ A y ↔ x ∈ A ∧ x F y
9 8 eubidv ⊢ A ∈ dom ⁡ F → ∃! y x F ↾ A y ↔ ∃! y x ∈ A ∧ x F y
10 9 ralbidv ⊢ A ∈ dom ⁡ F → ∀ x ∈ dom ⁡ F ↾ A ∃! y x F ↾ A y ↔ ∀ x ∈ dom ⁡ F ↾ A ∃! y x ∈ A ∧ x F y
11 eldmressnsn ⊢ A ∈ dom ⁡ F → A ∈ dom ⁡ F ↾ A
12 eldmressn ⊢ x ∈ dom ⁡ F ↾ A → x = A
13 velsn ⊢ x ∈ A ↔ x = A
14 13 biimpri ⊢ x = A → x ∈ A
15 breq1 ⊢ x = A → x F y ↔ A F y
16 15 anbi2d ⊢ x = A → x ∈ A ∧ x F y ↔ x ∈ A ∧ A F y
17 14 16 mpbirand ⊢ x = A → x ∈ A ∧ x F y ↔ A F y
18 17 eubidv ⊢ x = A → ∃! y x ∈ A ∧ x F y ↔ ∃! y A F y
19 11 12 18 ralbinrald ⊢ A ∈ dom ⁡ F → ∀ x ∈ dom ⁡ F ↾ A ∃! y x ∈ A ∧ x F y ↔ ∃! y A F y
20 10 19 bitrd ⊢ A ∈ dom ⁡ F → ∀ x ∈ dom ⁡ F ↾ A ∃! y x F ↾ A y ↔ ∃! y A F y
21 20 pm5.32i ⊢ A ∈ dom ⁡ F ∧ ∀ x ∈ dom ⁡ F ↾ A ∃! y x F ↾ A y ↔ A ∈ dom ⁡ F ∧ ∃! y A F y
22 1 5 21 3bitri ⊢ F defAt A ↔ A ∈ dom ⁡ F ∧ ∃! y A F y