Metamath Proof Explorer

Theorem reusv2lem4

Description: Lemma for reusv2 . (Contributed by NM, 13-Dec-2012)

Ref Expression
Assertion reusv2lem4 ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝑥 = 𝐶 ) ↔ ∃! 𝑥 ∀ 𝑦 ∈ 𝐵 ( ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 df-reu ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝑥 = 𝐶 ) ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝑥 = 𝐶 ) ) )
2 anass ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) ) ∧ 𝑥 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) ∧ 𝑥 = 𝐶 ) ) )
3 rabid ⊢ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) ) )
4 3 anbi1i ⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } ∧ 𝑥 = 𝐶 ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) ) ∧ 𝑥 = 𝐶 ) )
5 anass ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ 𝑥 = 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝑥 = 𝐶 ) ) )
6 eleq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
7 6 anbi1d ⊢ ( 𝑥 = 𝐶 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) ) )
8 7 pm5.32ri ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ 𝑥 = 𝐶 ) ↔ ( ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) ∧ 𝑥 = 𝐶 ) )
9 5 8 bitr3i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝑥 = 𝐶 ) ) ↔ ( ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) ∧ 𝑥 = 𝐶 ) )
10 9 anbi2i ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝑥 = 𝐶 ) ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) ∧ 𝑥 = 𝐶 ) ) )
11 2 4 10 3bitr4ri ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝑥 = 𝐶 ) ) ) ↔ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } ∧ 𝑥 = 𝐶 ) )
12 11 rexbii2 ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝑥 = 𝐶 ) ) ↔ ∃ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } 𝑥 = 𝐶 )
13 r19.42v ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝑥 = 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝑥 = 𝐶 ) ) )
14 nfrab1 ⊢ Ⅎ 𝑦 { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) }
15 nfcv ⊢ Ⅎ 𝑧 { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) }
16 nfv ⊢ Ⅎ 𝑧 𝑥 = 𝐶
17 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑦 ⦌ 𝐶
18 17 nfeq2 ⊢ Ⅎ 𝑦 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶
19 csbeq1a ⊢ ( 𝑦 = 𝑧 → 𝐶 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 )
20 19 eqeq2d ⊢ ( 𝑦 = 𝑧 → ( 𝑥 = 𝐶 ↔ 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ) )
21 14 15 16 18 20 cbvrexfw ⊢ ( ∃ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } 𝑥 = 𝐶 ↔ ∃ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 )
22 12 13 21 3bitr3i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝑥 = 𝐶 ) ) ↔ ∃ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 )
23 22 eubii ⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝑥 = 𝐶 ) ) ↔ ∃! 𝑥 ∃ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 )
24 elex ⊢ ( 𝐶 ∈ 𝐴 → 𝐶 ∈ V )
25 24 ad2antrl ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) ) → 𝐶 ∈ V )
26 3 25 sylbi ⊢ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } → 𝐶 ∈ V )
27 26 rgen ⊢ ∀ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } 𝐶 ∈ V
28 nfv ⊢ Ⅎ 𝑧 𝐶 ∈ V
29 17 nfel1 ⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ∈ V
30 19 eleq1d ⊢ ( 𝑦 = 𝑧 → ( 𝐶 ∈ V ↔ ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ∈ V ) )
31 14 15 28 29 30 cbvralfw ⊢ ( ∀ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } 𝐶 ∈ V ↔ ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ∈ V )
32 27 31 mpbi ⊢ ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ∈ V
33 reusv2lem3 ⊢ ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ∈ V → ( ∃! 𝑥 ∃ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ↔ ∃! 𝑥 ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ) )
34 32 33 ax-mp ⊢ ( ∃! 𝑥 ∃ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ↔ ∃! 𝑥 ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 )
35 df-ral ⊢ ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } → 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ) )
36 nfv ⊢ Ⅎ 𝑧 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } → 𝑥 = 𝐶 )
37 14 nfcri ⊢ Ⅎ 𝑦 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) }
38 37 18 nfim ⊢ Ⅎ 𝑦 ( 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } → 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 )
39 eleq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } ↔ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } ) )
40 39 20 imbi12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } → 𝑥 = 𝐶 ) ↔ ( 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } → 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ) ) )
41 36 38 40 cbvalv1 ⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } → 𝑥 = 𝐶 ) ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } → 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ) )
42 3 imbi1i ⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } → 𝑥 = 𝐶 ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) ) → 𝑥 = 𝐶 ) )
43 impexp ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) ) → 𝑥 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 → ( ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝐶 ) ) )
44 42 43 bitri ⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } → 𝑥 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 → ( ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝐶 ) ) )
45 44 albii ⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } → 𝑥 = 𝐶 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝐶 ) ) )
46 df-ral ⊢ ( ∀ 𝑦 ∈ 𝐵 ( ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝐶 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝐶 ) ) )
47 45 46 bitr4i ⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } → 𝑥 = 𝐶 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝐶 ) )
48 35 41 47 3bitr2i ⊢ ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝐶 ) )
49 48 eubii ⊢ ( ∃! 𝑥 ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ↔ ∃! 𝑥 ∀ 𝑦 ∈ 𝐵 ( ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝐶 ) )
50 34 49 bitri ⊢ ( ∃! 𝑥 ∃ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ↔ ∃! 𝑥 ∀ 𝑦 ∈ 𝐵 ( ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝐶 ) )
51 1 23 50 3bitri ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝑥 = 𝐶 ) ↔ ∃! 𝑥 ∀ 𝑦 ∈ 𝐵 ( ( 𝐶 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝐶 ) )