Metamath Proof Explorer

Theorem unirep

Description: Define a quantity whose definition involves a choice of representative, but which is uniquely determined regardless of the choice. (Contributed by Jeff Madsen, 1-Jun-2011)

Ref Expression
Hypotheses unirep.1 ⊢ ( 𝑦 = 𝐷 → ( 𝜑 ↔ 𝜓 ) )
unirep.2 ⊢ ( 𝑦 = 𝐷 → 𝐵 = 𝐶 )
unirep.3 ⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ 𝜒 ) )
unirep.4 ⊢ ( 𝑦 = 𝑧 → 𝐵 = 𝐹 )
unirep.5 ⊢ 𝐵 ∈ V
Assertion unirep ( ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ( 𝐷 ∈ 𝐴 ∧ 𝜓 ) ) → ( ℩ 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 unirep.1 ⊢ ( 𝑦 = 𝐷 → ( 𝜑 ↔ 𝜓 ) )
2 unirep.2 ⊢ ( 𝑦 = 𝐷 → 𝐵 = 𝐶 )
3 unirep.3 ⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ 𝜒 ) )
4 unirep.4 ⊢ ( 𝑦 = 𝑧 → 𝐵 = 𝐹 )
5 unirep.5 ⊢ 𝐵 ∈ V
6 eqidd ⊢ ( 𝜓 → 𝐶 = 𝐶 )
7 6 ancli ⊢ ( 𝜓 → ( 𝜓 ∧ 𝐶 = 𝐶 ) )
8 2 eqeq2d ⊢ ( 𝑦 = 𝐷 → ( 𝐶 = 𝐵 ↔ 𝐶 = 𝐶 ) )
9 1 8 anbi12d ⊢ ( 𝑦 = 𝐷 → ( ( 𝜑 ∧ 𝐶 = 𝐵 ) ↔ ( 𝜓 ∧ 𝐶 = 𝐶 ) ) )
10 9 rspcev ⊢ ( ( 𝐷 ∈ 𝐴 ∧ ( 𝜓 ∧ 𝐶 = 𝐶 ) ) → ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝐶 = 𝐵 ) )
11 7 10 sylan2 ⊢ ( ( 𝐷 ∈ 𝐴 ∧ 𝜓 ) → ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝐶 = 𝐵 ) )
12 11 adantl ⊢ ( ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ( 𝐷 ∈ 𝐴 ∧ 𝜓 ) ) → ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝐶 = 𝐵 ) )
13 nfcvd ⊢ ( 𝐷 ∈ 𝐴 → Ⅎ 𝑦 𝐶 )
14 13 2 csbiegf ⊢ ( 𝐷 ∈ 𝐴 → ⦋ 𝐷 / 𝑦 ⦌ 𝐵 = 𝐶 )
15 5 csbex ⊢ ⦋ 𝐷 / 𝑦 ⦌ 𝐵 ∈ V
16 14 15 eqeltrrdi ⊢ ( 𝐷 ∈ 𝐴 → 𝐶 ∈ V )
17 16 ad2antrl ⊢ ( ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ( 𝐷 ∈ 𝐴 ∧ 𝜓 ) ) → 𝐶 ∈ V )
18 eqeq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 = 𝐵 ↔ 𝐶 = 𝐵 ) )
19 18 anbi2d ⊢ ( 𝑥 = 𝐶 → ( ( 𝜑 ∧ 𝑥 = 𝐵 ) ↔ ( 𝜑 ∧ 𝐶 = 𝐵 ) ) )
20 19 rexbidv ⊢ ( 𝑥 = 𝐶 → ( ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝐶 = 𝐵 ) ) )
21 20 spcegv ⊢ ( 𝐶 ∈ V → ( ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝐶 = 𝐵 ) → ∃ 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) ) )
22 16 21 syl ⊢ ( 𝐷 ∈ 𝐴 → ( ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝐶 = 𝐵 ) → ∃ 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) ) )
23 22 adantr ⊢ ( ( 𝐷 ∈ 𝐴 ∧ 𝜓 ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝐶 = 𝐵 ) → ∃ 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) ) )
24 11 23 mpd ⊢ ( ( 𝐷 ∈ 𝐴 ∧ 𝜓 ) → ∃ 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) )
25 24 adantl ⊢ ( ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ( 𝐷 ∈ 𝐴 ∧ 𝜓 ) ) → ∃ 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) )
26 r19.29 ⊢ ( ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) ) → ∃ 𝑦 ∈ 𝐴 ( ∀ 𝑧 ∈ 𝐴 ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ( 𝜑 ∧ 𝑥 = 𝐵 ) ) )
27 r19.29 ⊢ ( ( ∀ 𝑧 ∈ 𝐴 ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ∃ 𝑧 ∈ 𝐴 ( 𝜒 ∧ 𝑤 = 𝐹 ) ) → ∃ 𝑧 ∈ 𝐴 ( ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ( 𝜒 ∧ 𝑤 = 𝐹 ) ) )
28 an4 ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝐵 ) ∧ ( 𝜒 ∧ 𝑤 = 𝐹 ) ) ↔ ( ( 𝜑 ∧ 𝜒 ) ∧ ( 𝑥 = 𝐵 ∧ 𝑤 = 𝐹 ) ) )
29 pm3.35 ⊢ ( ( ( 𝜑 ∧ 𝜒 ) ∧ ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ) → 𝐵 = 𝐹 )
30 eqeq12 ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑤 = 𝐹 ) → ( 𝑥 = 𝑤 ↔ 𝐵 = 𝐹 ) )
31 29 30 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝜒 ) ∧ ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ) → ( ( 𝑥 = 𝐵 ∧ 𝑤 = 𝐹 ) → 𝑥 = 𝑤 ) )
32 31 ancoms ⊢ ( ( ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ( 𝜑 ∧ 𝜒 ) ) → ( ( 𝑥 = 𝐵 ∧ 𝑤 = 𝐹 ) → 𝑥 = 𝑤 ) )
33 32 expimpd ⊢ ( ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) → ( ( ( 𝜑 ∧ 𝜒 ) ∧ ( 𝑥 = 𝐵 ∧ 𝑤 = 𝐹 ) ) → 𝑥 = 𝑤 ) )
34 28 33 syl5bi ⊢ ( ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) → ( ( ( 𝜑 ∧ 𝑥 = 𝐵 ) ∧ ( 𝜒 ∧ 𝑤 = 𝐹 ) ) → 𝑥 = 𝑤 ) )
35 34 ancomsd ⊢ ( ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) → ( ( ( 𝜒 ∧ 𝑤 = 𝐹 ) ∧ ( 𝜑 ∧ 𝑥 = 𝐵 ) ) → 𝑥 = 𝑤 ) )
36 35 expdimp ⊢ ( ( ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ( 𝜒 ∧ 𝑤 = 𝐹 ) ) → ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → 𝑥 = 𝑤 ) )
37 36 rexlimivw ⊢ ( ∃ 𝑧 ∈ 𝐴 ( ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ( 𝜒 ∧ 𝑤 = 𝐹 ) ) → ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → 𝑥 = 𝑤 ) )
38 37 imp ⊢ ( ( ∃ 𝑧 ∈ 𝐴 ( ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ( 𝜒 ∧ 𝑤 = 𝐹 ) ) ∧ ( 𝜑 ∧ 𝑥 = 𝐵 ) ) → 𝑥 = 𝑤 )
39 27 38 sylan ⊢ ( ( ( ∀ 𝑧 ∈ 𝐴 ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ∃ 𝑧 ∈ 𝐴 ( 𝜒 ∧ 𝑤 = 𝐹 ) ) ∧ ( 𝜑 ∧ 𝑥 = 𝐵 ) ) → 𝑥 = 𝑤 )
40 39 an32s ⊢ ( ( ( ∀ 𝑧 ∈ 𝐴 ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ( 𝜑 ∧ 𝑥 = 𝐵 ) ) ∧ ∃ 𝑧 ∈ 𝐴 ( 𝜒 ∧ 𝑤 = 𝐹 ) ) → 𝑥 = 𝑤 )
41 40 ex ⊢ ( ( ∀ 𝑧 ∈ 𝐴 ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ( 𝜑 ∧ 𝑥 = 𝐵 ) ) → ( ∃ 𝑧 ∈ 𝐴 ( 𝜒 ∧ 𝑤 = 𝐹 ) → 𝑥 = 𝑤 ) )
42 41 rexlimivw ⊢ ( ∃ 𝑦 ∈ 𝐴 ( ∀ 𝑧 ∈ 𝐴 ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ( 𝜑 ∧ 𝑥 = 𝐵 ) ) → ( ∃ 𝑧 ∈ 𝐴 ( 𝜒 ∧ 𝑤 = 𝐹 ) → 𝑥 = 𝑤 ) )
43 26 42 syl ⊢ ( ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) ) → ( ∃ 𝑧 ∈ 𝐴 ( 𝜒 ∧ 𝑤 = 𝐹 ) → 𝑥 = 𝑤 ) )
44 43 expimpd ⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) → ( ( ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) ∧ ∃ 𝑧 ∈ 𝐴 ( 𝜒 ∧ 𝑤 = 𝐹 ) ) → 𝑥 = 𝑤 ) )
45 44 adantr ⊢ ( ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ( 𝐷 ∈ 𝐴 ∧ 𝜓 ) ) → ( ( ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) ∧ ∃ 𝑧 ∈ 𝐴 ( 𝜒 ∧ 𝑤 = 𝐹 ) ) → 𝑥 = 𝑤 ) )
46 45 alrimivv ⊢ ( ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ( 𝐷 ∈ 𝐴 ∧ 𝜓 ) ) → ∀ 𝑥 ∀ 𝑤 ( ( ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) ∧ ∃ 𝑧 ∈ 𝐴 ( 𝜒 ∧ 𝑤 = 𝐹 ) ) → 𝑥 = 𝑤 ) )
47 eqeq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 = 𝐵 ↔ 𝑤 = 𝐵 ) )
48 47 anbi2d ⊢ ( 𝑥 = 𝑤 → ( ( 𝜑 ∧ 𝑥 = 𝐵 ) ↔ ( 𝜑 ∧ 𝑤 = 𝐵 ) ) )
49 48 rexbidv ⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑤 = 𝐵 ) ) )
50 4 eqeq2d ⊢ ( 𝑦 = 𝑧 → ( 𝑤 = 𝐵 ↔ 𝑤 = 𝐹 ) )
51 3 50 anbi12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝜑 ∧ 𝑤 = 𝐵 ) ↔ ( 𝜒 ∧ 𝑤 = 𝐹 ) ) )
52 51 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑤 = 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐴 ( 𝜒 ∧ 𝑤 = 𝐹 ) )
53 49 52 bitrdi ⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐴 ( 𝜒 ∧ 𝑤 = 𝐹 ) ) )
54 53 eu4 ⊢ ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) ↔ ( ∃ 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑤 ( ( ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) ∧ ∃ 𝑧 ∈ 𝐴 ( 𝜒 ∧ 𝑤 = 𝐹 ) ) → 𝑥 = 𝑤 ) ) )
55 25 46 54 sylanbrc ⊢ ( ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ( 𝐷 ∈ 𝐴 ∧ 𝜓 ) ) → ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) )
56 20 iota2 ⊢ ( ( 𝐶 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝐶 = 𝐵 ) ↔ ( ℩ 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) ) = 𝐶 ) )
57 17 55 56 syl2anc ⊢ ( ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ( 𝐷 ∈ 𝐴 ∧ 𝜓 ) ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝐶 = 𝐵 ) ↔ ( ℩ 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) ) = 𝐶 ) )
58 12 57 mpbid ⊢ ( ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝜑 ∧ 𝜒 ) → 𝐵 = 𝐹 ) ∧ ( 𝐷 ∈ 𝐴 ∧ 𝜓 ) ) → ( ℩ 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝑥 = 𝐵 ) ) = 𝐶 )