Metamath Proof Explorer


Theorem fiunlem

Description: Lemma for fiun and f1iun . Formerly part of f1iun . (Contributed by AV, 6-Oct-2023)

Ref Expression
Hypothesis fiun.1 ( 𝑥 = 𝑦𝐵 = 𝐶 )
Assertion fiunlem ( ( ( 𝐵 : 𝐷𝑆 ∧ ∀ 𝑦𝐴 ( 𝐵𝐶𝐶𝐵 ) ) ∧ 𝑢 = 𝐵 ) → ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥𝐴 𝑧 = 𝐵 } ( 𝑢𝑣𝑣𝑢 ) )

Proof

Step Hyp Ref Expression
1 fiun.1 ( 𝑥 = 𝑦𝐵 = 𝐶 )
2 vex 𝑣 ∈ V
3 eqeq1 ( 𝑧 = 𝑣 → ( 𝑧 = 𝐵𝑣 = 𝐵 ) )
4 3 rexbidv ( 𝑧 = 𝑣 → ( ∃ 𝑥𝐴 𝑧 = 𝐵 ↔ ∃ 𝑥𝐴 𝑣 = 𝐵 ) )
5 2 4 elab ( 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥𝐴 𝑧 = 𝐵 } ↔ ∃ 𝑥𝐴 𝑣 = 𝐵 )
6 1 eqeq2d ( 𝑥 = 𝑦 → ( 𝑣 = 𝐵𝑣 = 𝐶 ) )
7 6 cbvrexvw ( ∃ 𝑥𝐴 𝑣 = 𝐵 ↔ ∃ 𝑦𝐴 𝑣 = 𝐶 )
8 r19.29 ( ( ∀ 𝑦𝐴 ( 𝐵𝐶𝐶𝐵 ) ∧ ∃ 𝑦𝐴 𝑣 = 𝐶 ) → ∃ 𝑦𝐴 ( ( 𝐵𝐶𝐶𝐵 ) ∧ 𝑣 = 𝐶 ) )
9 sseq12 ( ( 𝑢 = 𝐵𝑣 = 𝐶 ) → ( 𝑢𝑣𝐵𝐶 ) )
10 9 ancoms ( ( 𝑣 = 𝐶𝑢 = 𝐵 ) → ( 𝑢𝑣𝐵𝐶 ) )
11 sseq12 ( ( 𝑣 = 𝐶𝑢 = 𝐵 ) → ( 𝑣𝑢𝐶𝐵 ) )
12 10 11 orbi12d ( ( 𝑣 = 𝐶𝑢 = 𝐵 ) → ( ( 𝑢𝑣𝑣𝑢 ) ↔ ( 𝐵𝐶𝐶𝐵 ) ) )
13 12 biimprcd ( ( 𝐵𝐶𝐶𝐵 ) → ( ( 𝑣 = 𝐶𝑢 = 𝐵 ) → ( 𝑢𝑣𝑣𝑢 ) ) )
14 13 expdimp ( ( ( 𝐵𝐶𝐶𝐵 ) ∧ 𝑣 = 𝐶 ) → ( 𝑢 = 𝐵 → ( 𝑢𝑣𝑣𝑢 ) ) )
15 14 rexlimivw ( ∃ 𝑦𝐴 ( ( 𝐵𝐶𝐶𝐵 ) ∧ 𝑣 = 𝐶 ) → ( 𝑢 = 𝐵 → ( 𝑢𝑣𝑣𝑢 ) ) )
16 15 imp ( ( ∃ 𝑦𝐴 ( ( 𝐵𝐶𝐶𝐵 ) ∧ 𝑣 = 𝐶 ) ∧ 𝑢 = 𝐵 ) → ( 𝑢𝑣𝑣𝑢 ) )
17 8 16 sylan ( ( ( ∀ 𝑦𝐴 ( 𝐵𝐶𝐶𝐵 ) ∧ ∃ 𝑦𝐴 𝑣 = 𝐶 ) ∧ 𝑢 = 𝐵 ) → ( 𝑢𝑣𝑣𝑢 ) )
18 17 an32s ( ( ( ∀ 𝑦𝐴 ( 𝐵𝐶𝐶𝐵 ) ∧ 𝑢 = 𝐵 ) ∧ ∃ 𝑦𝐴 𝑣 = 𝐶 ) → ( 𝑢𝑣𝑣𝑢 ) )
19 18 adantlll ( ( ( ( 𝐵 : 𝐷𝑆 ∧ ∀ 𝑦𝐴 ( 𝐵𝐶𝐶𝐵 ) ) ∧ 𝑢 = 𝐵 ) ∧ ∃ 𝑦𝐴 𝑣 = 𝐶 ) → ( 𝑢𝑣𝑣𝑢 ) )
20 7 19 sylan2b ( ( ( ( 𝐵 : 𝐷𝑆 ∧ ∀ 𝑦𝐴 ( 𝐵𝐶𝐶𝐵 ) ) ∧ 𝑢 = 𝐵 ) ∧ ∃ 𝑥𝐴 𝑣 = 𝐵 ) → ( 𝑢𝑣𝑣𝑢 ) )
21 5 20 sylan2b ( ( ( ( 𝐵 : 𝐷𝑆 ∧ ∀ 𝑦𝐴 ( 𝐵𝐶𝐶𝐵 ) ) ∧ 𝑢 = 𝐵 ) ∧ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥𝐴 𝑧 = 𝐵 } ) → ( 𝑢𝑣𝑣𝑢 ) )
22 21 ralrimiva ( ( ( 𝐵 : 𝐷𝑆 ∧ ∀ 𝑦𝐴 ( 𝐵𝐶𝐶𝐵 ) ) ∧ 𝑢 = 𝐵 ) → ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥𝐴 𝑧 = 𝐵 } ( 𝑢𝑣𝑣𝑢 ) )