This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qliftfuns

Description: The function F is the unique function defined by F[ x ] = A , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016) (Revised by AV, 3-Aug-2024)

Ref Expression
Hypotheses qlift.1 ⊢ F = ran ⁡ x ∈ X ⟼ x R A
qlift.2 ⊢ φ ∧ x ∈ X → A ∈ Y
qlift.3 ⊢ φ → R Er X
qlift.4 ⊢ φ → X ∈ V
Assertion qliftfuns ⊢ φ → Fun ⁡ F ↔ ∀ y ∀ z y R z → ⦋ y / x⦌ A = ⦋ z / x⦌ A

Proof

Step Hyp Ref Expression
1 qlift.1 ⊢ F = ran ⁡ x ∈ X ⟼ x R A
2 qlift.2 ⊢ φ ∧ x ∈ X → A ∈ Y
3 qlift.3 ⊢ φ → R Er X
4 qlift.4 ⊢ φ → X ∈ V
5 nfcv ⊢ Ⅎ _ y x R A
6 nfcv ⊢ Ⅎ _ x y R
7 nfcsb1v ⊢ Ⅎ _ x ⦋ y / x⦌ A
8 6 7 nfop ⊢ Ⅎ _ x y R ⦋ y / x⦌ A
9 eceq1 ⊢ x = y → x R = y R
10 csbeq1a ⊢ x = y → A = ⦋ y / x⦌ A
11 9 10 opeq12d ⊢ x = y → x R A = y R ⦋ y / x⦌ A
12 5 8 11 cbvmpt ⊢ x ∈ X ⟼ x R A = y ∈ X ⟼ y R ⦋ y / x⦌ A
13 12 rneqi ⊢ ran ⁡ x ∈ X ⟼ x R A = ran ⁡ y ∈ X ⟼ y R ⦋ y / x⦌ A
14 1 13 eqtri ⊢ F = ran ⁡ y ∈ X ⟼ y R ⦋ y / x⦌ A
15 2 ralrimiva ⊢ φ → ∀ x ∈ X A ∈ Y
16 7 nfel1 ⊢ Ⅎ x ⦋ y / x⦌ A ∈ Y
17 10 eleq1d ⊢ x = y → A ∈ Y ↔ ⦋ y / x⦌ A ∈ Y
18 16 17 rspc ⊢ y ∈ X → ∀ x ∈ X A ∈ Y → ⦋ y / x⦌ A ∈ Y
19 15 18 mpan9 ⊢ φ ∧ y ∈ X → ⦋ y / x⦌ A ∈ Y
20 csbeq1 ⊢ y = z → ⦋ y / x⦌ A = ⦋ z / x⦌ A
21 14 19 3 4 20 qliftfun ⊢ φ → Fun ⁡ F ↔ ∀ y ∀ z y R z → ⦋ y / x⦌ A = ⦋ z / x⦌ A