Theorem dfafv2

Description: Alternative definition of ( F ''' A ) using ( FA ) directly. (Contributed by Alexander van der Vekens, 22-Jul-2017) (Revised by AV, 25-Aug-2022)

	Ref	Expression
Assertion	dfafv2	⊢ ( 𝐹 ''' 𝐴 ) = if ( 𝐹 defAt 𝐴 , ( 𝐹 ‘ 𝐴 ) , V )

Proof

Step	Hyp	Ref	Expression
1		df-fv	⊢ ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑥 𝐴 𝐹 𝑥 )
2		simprr	⊢ ( ( ⊤ ∧ ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) ) → ∃! 𝑥 𝐴 𝐹 𝑥 )
3		reuaiotaiota	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 ↔ ( ℩ 𝑥 𝐴 𝐹 𝑥 ) = ( ℩' 𝑥 𝐴 𝐹 𝑥 ) )
4	2 3	sylib	⊢ ( ( ⊤ ∧ ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) ) → ( ℩ 𝑥 𝐴 𝐹 𝑥 ) = ( ℩' 𝑥 𝐴 𝐹 𝑥 ) )
5	1 4	eqtrid	⊢ ( ( ⊤ ∧ ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) ) → ( 𝐹 ‘ 𝐴 ) = ( ℩' 𝑥 𝐴 𝐹 𝑥 ) )
6		eubrdm	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 → 𝐴 ∈ dom 𝐹 )
7	6	ancri	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) )
8	7	con3i	⊢ ( ¬ ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) → ¬ ∃! 𝑥 𝐴 𝐹 𝑥 )
9	8	adantl	⊢ ( ( ⊤ ∧ ¬ ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) ) → ¬ ∃! 𝑥 𝐴 𝐹 𝑥 )
10		aiotavb	⊢ ( ¬ ∃! 𝑥 𝐴 𝐹 𝑥 ↔ ( ℩' 𝑥 𝐴 𝐹 𝑥 ) = V )
11	9 10	sylib	⊢ ( ( ⊤ ∧ ¬ ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) ) → ( ℩' 𝑥 𝐴 𝐹 𝑥 ) = V )
12	11	eqcomd	⊢ ( ( ⊤ ∧ ¬ ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) ) → V = ( ℩' 𝑥 𝐴 𝐹 𝑥 ) )
13	5 12	ifeqda	⊢ ( ⊤ → if ( ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) , ( 𝐹 ‘ 𝐴 ) , V ) = ( ℩' 𝑥 𝐴 𝐹 𝑥 ) )
14	13	mptru	⊢ if ( ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) , ( 𝐹 ‘ 𝐴 ) , V ) = ( ℩' 𝑥 𝐴 𝐹 𝑥 )
15		dfdfat2	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) )
16		ifbi	⊢ ( ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) ) → if ( 𝐹 defAt 𝐴 , ( 𝐹 ‘ 𝐴 ) , V ) = if ( ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) , ( 𝐹 ‘ 𝐴 ) , V ) )
17	15 16	ax-mp	⊢ if ( 𝐹 defAt 𝐴 , ( 𝐹 ‘ 𝐴 ) , V ) = if ( ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) , ( 𝐹 ‘ 𝐴 ) , V )
18		df-afv	⊢ ( 𝐹 ''' 𝐴 ) = ( ℩' 𝑥 𝐴 𝐹 𝑥 )
19	14 17 18	3eqtr4ri	⊢ ( 𝐹 ''' 𝐴 ) = if ( 𝐹 defAt 𝐴 , ( 𝐹 ‘ 𝐴 ) , V )