Metamath Proof Explorer

Theorem unielss

Description: Two ways to say the union of a class is an element of a subclass. (Contributed by RP, 29-Jan-2025)

Ref Expression
Assertion unielss ( 𝐴 ⊆ 𝐵 → ( ∪ 𝐵 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 uniel ⊢ ( ∪ 𝐵 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) )
2 df-ss ⊢ ( 𝑦 ⊆ 𝑥 ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) )
3 2 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) )
4 df-ral ⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ∀ 𝑧 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) )
5 19.21v ⊢ ( ∀ 𝑧 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑦 ∈ 𝐵 → ∀ 𝑧 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) )
6 5 albii ⊢ ( ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ∀ 𝑧 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) )
7 alcom ⊢ ( ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) ↔ ∀ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) )
8 4 6 7 3bitr2i ⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) )
9 3 8 bitri ⊢ ( ∀ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 ↔ ∀ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) )
10 ssel2 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
11 pm2.27 ⊢ ( 𝑧 ∈ 𝑥 → ( ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
12 elequ2 ⊢ ( 𝑦 = 𝑥 → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑥 ) )
13 12 imbi1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ↔ ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) ) )
14 13 12 imbi12d ⊢ ( 𝑦 = 𝑥 → ( ( ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ( ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ) )
15 14 rspcev ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ( ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) ) → ∃ 𝑦 ∈ 𝐵 ( ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
16 10 11 15 syl2an ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝑥 ) → ∃ 𝑦 ∈ 𝐵 ( ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
17 r19.35 ⊢ ( ∃ 𝑦 ∈ 𝐵 ( ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ( ∀ 𝑦 ∈ 𝐵 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) → ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) )
18 df-ral ⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) )
19 18 imbi1i ⊢ ( ( ∀ 𝑦 ∈ 𝐵 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) → ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) ↔ ( ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) → ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) )
20 17 19 bitri ⊢ ( ∃ 𝑦 ∈ 𝐵 ( ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ( ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) → ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) )
21 16 20 sylib ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝑥 ) → ( ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) → ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) )
22 21 impancom ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) ) → ( 𝑧 ∈ 𝑥 → ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) )
23 nfv ⊢ Ⅎ 𝑦 ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 )
24 nfa1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) )
25 23 24 nfan ⊢ Ⅎ 𝑦 ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) )
26 nfv ⊢ Ⅎ 𝑦 𝑧 ∈ 𝑥
27 sp ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) → ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) )
28 27 adantl ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) ) → ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) )
29 25 26 28 rexlimd ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) ) → ( ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) )
30 22 29 impbid ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) ) → ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) )
31 rspe ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑦 ) → ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 )
32 31 ex ⊢ ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) )
33 32 ax-gen ⊢ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) )
34 nfre1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦
35 26 34 nfbi ⊢ Ⅎ 𝑦 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 )
36 imbi2 ⊢ ( ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) → ( ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ↔ ( 𝑧 ∈ 𝑦 → ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) ) )
37 36 imbi2d ⊢ ( ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) → ( ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) ) ) )
38 35 37 albid ⊢ ( ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) → ( ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) ) ) )
39 38 adantl ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) ) → ( ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) ) ) )
40 33 39 mpbiri ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) ) → ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) )
41 30 40 impbida ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) ) )
42 41 albidv ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) ) )
43 9 42 bitrid ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) ) )
44 43 rexbidva ⊢ ( 𝐴 ⊆ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝑦 ) ) )
45 1 44 bitr4id ⊢ ( 𝐴 ⊆ 𝐵 → ( ∪ 𝐵 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 ) )