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

Metamath Proof Explorer

Theorem fliftfuns

Description: The function F is the unique function defined by FA = B , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016)

Ref Expression
Hypotheses flift.1 ⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
flift.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
flift.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
Assertion fliftfuns ( 𝜑 → ( Fun 𝐹 ↔ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 flift.1 ⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
2 flift.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑅 )
3 flift.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
4 nfcv ⊢ Ⅎ 𝑦 ⟨ 𝐴 , 𝐵 ⟩
5 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐴
6 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
7 5 6 nfop ⊢ Ⅎ 𝑥 ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩
8 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
9 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
10 8 9 opeq12d ⊢ ( 𝑥 = 𝑦 → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ )
11 4 7 10 cbvmpt ⊢ ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝑦 ∈ 𝑋 ↦ ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ )
12 11 rneqi ⊢ ran ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) = ran ( 𝑦 ∈ 𝑋 ↦ ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ )
13 1 12 eqtri ⊢ 𝐹 = ran ( 𝑦 ∈ 𝑋 ↦ ⟨ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ⟩ )
14 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐴 ∈ 𝑅 )
15 5 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ 𝑅
16 8 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝑅 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ 𝑅 ) )
17 15 16 rspc ⊢ ( 𝑦 ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 𝐴 ∈ 𝑅 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ 𝑅 ) )
18 14 17 mpan9 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ 𝑅 )
19 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑆 )
20 6 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑆
21 9 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ∈ 𝑆 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑆 ) )
22 20 21 rspc ⊢ ( 𝑦 ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑆 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑆 ) )
23 19 22 mpan9 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑆 )
24 csbeq1 ⊢ ( 𝑦 = 𝑧 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 )
25 csbeq1 ⊢ ( 𝑦 = 𝑧 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
26 13 18 23 24 25 fliftfun ⊢ ( 𝜑 → ( Fun 𝐹 ↔ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )