Metamath Proof Explorer

Theorem qliftfun

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 ⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ [ 𝑥 ] 𝑅 , 𝐴 ⟩ )
qlift.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑌 )
qlift.3 ⊢ ( 𝜑 → 𝑅 Er 𝑋 )
qlift.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
qliftfun.4 ⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
Assertion qliftfun ( 𝜑 → ( Fun 𝐹 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝐴 = 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 qlift.1 ⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ [ 𝑥 ] 𝑅 , 𝐴 ⟩ )
2 qlift.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑌 )
3 qlift.3 ⊢ ( 𝜑 → 𝑅 Er 𝑋 )
4 qlift.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
5 qliftfun.4 ⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
6 1 2 3 4 qliftlem ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → [ 𝑥 ] 𝑅 ∈ ( 𝑋 / 𝑅 ) )
7 eceq1 ⊢ ( 𝑥 = 𝑦 → [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 )
8 1 6 2 7 5 fliftfun ⊢ ( 𝜑 → ( Fun 𝐹 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 → 𝐴 = 𝐵 ) ) )
9 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝑅 Er 𝑋 )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝑥 𝑅 𝑦 )
11 9 10 ercl ⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ 𝑋 )
12 9 10 ercl2 ⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 ∈ 𝑋 )
13 11 12 jca ⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) )
14 13 ex ⊢ ( 𝜑 → ( 𝑥 𝑅 𝑦 → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) )
15 14 pm4.71rd ⊢ ( 𝜑 → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑅 𝑦 ) ) )
16 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑅 Er 𝑋 )
17 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
18 16 17 erth ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑅 𝑦 ↔ [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ) )
19 18 pm5.32da ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑅 𝑦 ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ) ) )
20 15 19 bitrd ⊢ ( 𝜑 → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ) ) )
21 20 imbi1d ⊢ ( 𝜑 → ( ( 𝑥 𝑅 𝑦 → 𝐴 = 𝐵 ) ↔ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ) → 𝐴 = 𝐵 ) ) )
22 impexp ⊢ ( ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ) → 𝐴 = 𝐵 ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 → 𝐴 = 𝐵 ) ) )
23 21 22 bitrdi ⊢ ( 𝜑 → ( ( 𝑥 𝑅 𝑦 → 𝐴 = 𝐵 ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 → 𝐴 = 𝐵 ) ) ) )
24 23 2albidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝐴 = 𝐵 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 → 𝐴 = 𝐵 ) ) ) )
25 r2al ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 → 𝐴 = 𝐵 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 → 𝐴 = 𝐵 ) ) )
26 24 25 bitr4di ⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝐴 = 𝐵 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 → 𝐴 = 𝐵 ) ) )
27 8 26 bitr4d ⊢ ( 𝜑 → ( Fun 𝐹 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝐴 = 𝐵 ) ) )