Theorem reusv2lem2

Description: Lemma for reusv2 . (Contributed by NM, 27-Oct-2010) (Proof shortened by Mario Carneiro, 19-Nov-2016) (Proof shortened by JJ, 7-Aug-2021)

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

Proof

Step	Hyp	Ref	Expression
1		eunex	⊢ ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑥 ¬ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
2		exnal	⊢ ( ∃ 𝑥 ¬ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ¬ ∀ 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
3	1 2	sylib	⊢ ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ¬ ∀ 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
4		rzal	⊢ ( 𝐴 = ∅ → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
5	4	alrimiv	⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
6	3 5	nsyl3	⊢ ( 𝐴 = ∅ → ¬ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
7	6	pm2.21d	⊢ ( 𝐴 = ∅ → ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
8		simpr	⊢ ( ( 𝐴 ≠ ∅ ∧ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
9		nfra1	⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵
10		nfra1	⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵
11		simpr	⊢ ( ( ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 = 𝐵 ) → 𝑥 = 𝐵 )
12		rspa	⊢ ( ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 = 𝐵 )
13	12	adantr	⊢ ( ( ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 = 𝐵 ) → 𝑧 = 𝐵 )
14	11 13	eqtr4d	⊢ ( ( ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 = 𝐵 ) → 𝑥 = 𝑧 )
15		eqeq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝐵 ↔ 𝑧 = 𝐵 ) )
16	15	ralbidv	⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ) )
17	16	biimprcd	⊢ ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 → ( 𝑥 = 𝑧 → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
18	17	ad2antrr	⊢ ( ( ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 = 𝐵 ) → ( 𝑥 = 𝑧 → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
19	14 18	mpd	⊢ ( ( ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 = 𝐵 ) → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
20	19	exp31	⊢ ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 → ( 𝑦 ∈ 𝐴 → ( 𝑥 = 𝐵 → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) ) )
21	9 10 20	rexlimd	⊢ ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
22	21	adantl	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
23		r19.2z	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
24	23	ex	⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
25	24	adantr	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ) → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
26	22 25	impbid	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
27	26	eubidv	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ) → ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
28	27	ex	⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 → ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) ) )
29	28	exlimdv	⊢ ( 𝐴 ≠ ∅ → ( ∃ 𝑧 ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 → ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) ) )
30		euex	⊢ ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
31	16	cbvexvw	⊢ ( ∃ 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃ 𝑧 ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 )
32	30 31	sylib	⊢ ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑧 ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 )
33	29 32	impel	⊢ ( ( 𝐴 ≠ ∅ ∧ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
34	8 33	mpbird	⊢ ( ( 𝐴 ≠ ∅ ∧ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
35	34	ex	⊢ ( 𝐴 ≠ ∅ → ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
36	7 35	pm2.61ine	⊢ ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )