Theorem reusv2lem3

Description: Lemma for reusv2 . (Contributed by NM, 14-Dec-2012) (Proof shortened by Mario Carneiro, 19-Nov-2016)

	Ref	Expression
Assertion	reusv2lem3	⊢ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V → ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
2		nfv	⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V
3		nfeu1	⊢ Ⅎ 𝑥 ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵
4	2 3	nfan	⊢ Ⅎ 𝑥 ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
5		euex	⊢ ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
6		rexn0	⊢ ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → 𝐴 ≠ ∅ )
7	6	exlimiv	⊢ ( ∃ 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → 𝐴 ≠ ∅ )
8		r19.2z	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
9	8	ex	⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
10	5 7 9	3syl	⊢ ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
11	10	adantl	⊢ ( ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
12		nfra1	⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V
13		nfre1	⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵
14	13	nfeuw	⊢ Ⅎ 𝑦 ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵
15	12 14	nfan	⊢ Ⅎ 𝑦 ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
16		rsp	⊢ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V → ( 𝑦 ∈ 𝐴 → 𝐵 ∈ V ) )
17	16	impcom	⊢ ( ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ) → 𝐵 ∈ V )
18		isset	⊢ ( 𝐵 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐵 )
19	17 18	sylib	⊢ ( ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ) → ∃ 𝑥 𝑥 = 𝐵 )
20	19	adantrr	⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) ) → ∃ 𝑥 𝑥 = 𝐵 )
21		rspe	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 = 𝐵 ) → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
22	21	ex	⊢ ( 𝑦 ∈ 𝐴 → ( 𝑥 = 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
23	22	ancrd	⊢ ( 𝑦 ∈ 𝐴 → ( 𝑥 = 𝐵 → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ∧ 𝑥 = 𝐵 ) ) )
24	23	eximdv	⊢ ( 𝑦 ∈ 𝐴 → ( ∃ 𝑥 𝑥 = 𝐵 → ∃ 𝑥 ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ∧ 𝑥 = 𝐵 ) ) )
25	24	imp	⊢ ( ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 𝑥 = 𝐵 ) → ∃ 𝑥 ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ∧ 𝑥 = 𝐵 ) )
26	20 25	syldan	⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) ) → ∃ 𝑥 ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ∧ 𝑥 = 𝐵 ) )
27		eupick	⊢ ( ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ∧ ∃ 𝑥 ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ∧ 𝑥 = 𝐵 ) ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → 𝑥 = 𝐵 ) )
28	1 26 27	syl2an2	⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → 𝑥 = 𝐵 ) )
29	28	ex	⊢ ( 𝑦 ∈ 𝐴 → ( ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → 𝑥 = 𝐵 ) ) )
30	29	com3l	⊢ ( ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ( 𝑦 ∈ 𝐴 → 𝑥 = 𝐵 ) ) )
31	15 13 30	ralrimd	⊢ ( ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
32	11 31	impbid	⊢ ( ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
33	4 32	eubid	⊢ ( ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
34	1 33	mpbird	⊢ ( ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
35	34	ex	⊢ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V → ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
36		reusv2lem2	⊢ ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
37	35 36	impbid1	⊢ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V → ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )