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 ⊢ ( ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) → ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) )