Metamath Proof Explorer

Theorem riotasvd

Description: Deduction version of riotasv . (Contributed by NM, 4-Mar-2013) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses riotasvd.1 ⊢ ( 𝜑 → 𝐷 = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) )
riotasvd.2 ⊢ ( 𝜑 → 𝐷 ∈ 𝐴 )
Assertion riotasvd ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) → 𝐷 = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 riotasvd.1 ⊢ ( 𝜑 → 𝐷 = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) )
2 riotasvd.2 ⊢ ( 𝜑 → 𝐷 ∈ 𝐴 )
3 1 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → 𝐷 = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) )
4 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → 𝐷 ∈ 𝐴 )
5 3 4 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) ∈ 𝐴 )
6 riotaclbgBAD ⊢ ( 𝐴 ∈ 𝑉 → ( ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ↔ ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) ∈ 𝐴 ) )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ↔ ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) ∈ 𝐴 ) )
8 5 7 mpbird ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) )
9 riotasbc ⊢ ( ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) → [ ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) / 𝑥 ] ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) )
10 8 9 syl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → [ ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) / 𝑥 ] ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) )
11 eqeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝐶 ↔ 𝑧 = 𝐶 ) )
12 11 imbi2d ⊢ ( 𝑥 = 𝑧 → ( ( 𝜓 → 𝑥 = 𝐶 ) ↔ ( 𝜓 → 𝑧 = 𝐶 ) ) )
13 12 ralbidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑧 = 𝐶 ) ) )
14 nfra1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 )
15 nfcv ⊢ Ⅎ 𝑦 𝐴
16 14 15 nfriota ⊢ Ⅎ 𝑦 ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) )
17 16 nfeq2 ⊢ Ⅎ 𝑦 𝑧 = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) )
18 eqeq1 ⊢ ( 𝑧 = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) → ( 𝑧 = 𝐶 ↔ ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) = 𝐶 ) )
19 18 imbi2d ⊢ ( 𝑧 = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) → ( ( 𝜓 → 𝑧 = 𝐶 ) ↔ ( 𝜓 → ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) = 𝐶 ) ) )
20 17 19 ralbid ⊢ ( 𝑧 = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑧 = 𝐶 ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝜓 → ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) = 𝐶 ) ) )
21 13 20 sbcie2g ⊢ ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) ∈ 𝐴 → ( [ ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) / 𝑥 ] ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝜓 → ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) = 𝐶 ) ) )
22 5 21 syl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( [ ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) / 𝑥 ] ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝜓 → ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) = 𝐶 ) ) )
23 10 22 mpbid ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ∀ 𝑦 ∈ 𝐵 ( 𝜓 → ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) = 𝐶 ) )
24 rsp ⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝜓 → ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) = 𝐶 ) → ( 𝑦 ∈ 𝐵 → ( 𝜓 → ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) = 𝐶 ) ) )
25 23 24 syl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑦 ∈ 𝐵 → ( 𝜓 → ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) = 𝐶 ) ) )
26 25 impd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) → ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) = 𝐶 ) )
27 3 eqeq1d ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐷 = 𝐶 ↔ ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) = 𝐶 ) )
28 26 27 sylibrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) → 𝐷 = 𝐶 ) )