Step | Hyp | Ref
| Expression |
1 | | sseq1 3926 |
. . . . . 6
⊢ (𝑎 = ∅ → (𝑎 ⊆ ∪ 𝐴
↔ ∅ ⊆ ∪ 𝐴)) |
2 | | sseq1 3926 |
. . . . . . 7
⊢ (𝑎 = ∅ → (𝑎 ⊆ 𝑧 ↔ ∅ ⊆ 𝑧)) |
3 | 2 | rexbidv 3216 |
. . . . . 6
⊢ (𝑎 = ∅ → (∃𝑧 ∈ 𝐴 𝑎 ⊆ 𝑧 ↔ ∃𝑧 ∈ 𝐴 ∅ ⊆ 𝑧)) |
4 | 1, 3 | imbi12d 348 |
. . . . 5
⊢ (𝑎 = ∅ → ((𝑎 ⊆ ∪ 𝐴
→ ∃𝑧 ∈
𝐴 𝑎 ⊆ 𝑧) ↔ (∅ ⊆ ∪ 𝐴
→ ∃𝑧 ∈
𝐴 ∅ ⊆ 𝑧))) |
5 | 4 | imbi2d 344 |
. . . 4
⊢ (𝑎 = ∅ → (((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
→ (𝑎 ⊆ ∪ 𝐴
→ ∃𝑧 ∈
𝐴 𝑎 ⊆ 𝑧)) ↔ ((𝐴 ≠ ∅ ∧ [⊊] Or
𝐴) → (∅ ⊆
∪ 𝐴 → ∃𝑧 ∈ 𝐴 ∅ ⊆ 𝑧)))) |
6 | | sseq1 3926 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (𝑎 ⊆ ∪ 𝐴 ↔ 𝑏 ⊆ ∪ 𝐴)) |
7 | | sseq1 3926 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → (𝑎 ⊆ 𝑧 ↔ 𝑏 ⊆ 𝑧)) |
8 | 7 | rexbidv 3216 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (∃𝑧 ∈ 𝐴 𝑎 ⊆ 𝑧 ↔ ∃𝑧 ∈ 𝐴 𝑏 ⊆ 𝑧)) |
9 | 6, 8 | imbi12d 348 |
. . . . 5
⊢ (𝑎 = 𝑏 → ((𝑎 ⊆ ∪ 𝐴 → ∃𝑧 ∈ 𝐴 𝑎 ⊆ 𝑧) ↔ (𝑏 ⊆ ∪ 𝐴 → ∃𝑧 ∈ 𝐴 𝑏 ⊆ 𝑧))) |
10 | 9 | imbi2d 344 |
. . . 4
⊢ (𝑎 = 𝑏 → (((𝐴 ≠ ∅ ∧ [⊊] Or
𝐴) → (𝑎 ⊆ ∪ 𝐴
→ ∃𝑧 ∈
𝐴 𝑎 ⊆ 𝑧)) ↔ ((𝐴 ≠ ∅ ∧ [⊊] Or
𝐴) → (𝑏 ⊆ ∪ 𝐴
→ ∃𝑧 ∈
𝐴 𝑏 ⊆ 𝑧)))) |
11 | | sseq1 3926 |
. . . . . 6
⊢ (𝑎 = (𝑏 ∪ {𝑐}) → (𝑎 ⊆ ∪ 𝐴 ↔ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴)) |
12 | | sseq1 3926 |
. . . . . . 7
⊢ (𝑎 = (𝑏 ∪ {𝑐}) → (𝑎 ⊆ 𝑧 ↔ (𝑏 ∪ {𝑐}) ⊆ 𝑧)) |
13 | 12 | rexbidv 3216 |
. . . . . 6
⊢ (𝑎 = (𝑏 ∪ {𝑐}) → (∃𝑧 ∈ 𝐴 𝑎 ⊆ 𝑧 ↔ ∃𝑧 ∈ 𝐴 (𝑏 ∪ {𝑐}) ⊆ 𝑧)) |
14 | 11, 13 | imbi12d 348 |
. . . . 5
⊢ (𝑎 = (𝑏 ∪ {𝑐}) → ((𝑎 ⊆ ∪ 𝐴 → ∃𝑧 ∈ 𝐴 𝑎 ⊆ 𝑧) ↔ ((𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴 → ∃𝑧 ∈ 𝐴 (𝑏 ∪ {𝑐}) ⊆ 𝑧))) |
15 | 14 | imbi2d 344 |
. . . 4
⊢ (𝑎 = (𝑏 ∪ {𝑐}) → (((𝐴 ≠ ∅ ∧ [⊊] Or
𝐴) → (𝑎 ⊆ ∪ 𝐴
→ ∃𝑧 ∈
𝐴 𝑎 ⊆ 𝑧)) ↔ ((𝐴 ≠ ∅ ∧ [⊊] Or
𝐴) → ((𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴 → ∃𝑧 ∈ 𝐴 (𝑏 ∪ {𝑐}) ⊆ 𝑧)))) |
16 | | sseq1 3926 |
. . . . . 6
⊢ (𝑎 = 𝐵 → (𝑎 ⊆ ∪ 𝐴 ↔ 𝐵 ⊆ ∪ 𝐴)) |
17 | | sseq1 3926 |
. . . . . . 7
⊢ (𝑎 = 𝐵 → (𝑎 ⊆ 𝑧 ↔ 𝐵 ⊆ 𝑧)) |
18 | 17 | rexbidv 3216 |
. . . . . 6
⊢ (𝑎 = 𝐵 → (∃𝑧 ∈ 𝐴 𝑎 ⊆ 𝑧 ↔ ∃𝑧 ∈ 𝐴 𝐵 ⊆ 𝑧)) |
19 | 16, 18 | imbi12d 348 |
. . . . 5
⊢ (𝑎 = 𝐵 → ((𝑎 ⊆ ∪ 𝐴 → ∃𝑧 ∈ 𝐴 𝑎 ⊆ 𝑧) ↔ (𝐵 ⊆ ∪ 𝐴 → ∃𝑧 ∈ 𝐴 𝐵 ⊆ 𝑧))) |
20 | 19 | imbi2d 344 |
. . . 4
⊢ (𝑎 = 𝐵 → (((𝐴 ≠ ∅ ∧ [⊊] Or
𝐴) → (𝑎 ⊆ ∪ 𝐴
→ ∃𝑧 ∈
𝐴 𝑎 ⊆ 𝑧)) ↔ ((𝐴 ≠ ∅ ∧ [⊊] Or
𝐴) → (𝐵 ⊆ ∪ 𝐴
→ ∃𝑧 ∈
𝐴 𝐵 ⊆ 𝑧)))) |
21 | | 0ss 4311 |
. . . . . . . 8
⊢ ∅
⊆ 𝑧 |
22 | 21 | rgenw 3073 |
. . . . . . 7
⊢
∀𝑧 ∈
𝐴 ∅ ⊆ 𝑧 |
23 | | r19.2z 4406 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧
∀𝑧 ∈ 𝐴 ∅ ⊆ 𝑧) → ∃𝑧 ∈ 𝐴 ∅ ⊆ 𝑧) |
24 | 22, 23 | mpan2 691 |
. . . . . 6
⊢ (𝐴 ≠ ∅ →
∃𝑧 ∈ 𝐴 ∅ ⊆ 𝑧) |
25 | 24 | adantr 484 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
→ ∃𝑧 ∈
𝐴 ∅ ⊆ 𝑧) |
26 | 25 | a1d 25 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
→ (∅ ⊆ ∪ 𝐴 → ∃𝑧 ∈ 𝐴 ∅ ⊆ 𝑧)) |
27 | | id 22 |
. . . . . . . . 9
⊢ ((𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴 → (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴) |
28 | 27 | unssad 4101 |
. . . . . . . 8
⊢ ((𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴 → 𝑏 ⊆ ∪ 𝐴) |
29 | 28 | imim1i 63 |
. . . . . . 7
⊢ ((𝑏 ⊆ ∪ 𝐴
→ ∃𝑧 ∈
𝐴 𝑏 ⊆ 𝑧) → ((𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴 → ∃𝑧 ∈ 𝐴 𝑏 ⊆ 𝑧)) |
30 | | sseq2 3927 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑤 → (𝑏 ⊆ 𝑧 ↔ 𝑏 ⊆ 𝑤)) |
31 | 30 | cbvrexvw 3359 |
. . . . . . . . . 10
⊢
(∃𝑧 ∈
𝐴 𝑏 ⊆ 𝑧 ↔ ∃𝑤 ∈ 𝐴 𝑏 ⊆ 𝑤) |
32 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
∧ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴)
→ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴) |
33 | 32 | unssbd 4102 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
∧ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴)
→ {𝑐} ⊆ ∪ 𝐴) |
34 | | vex 3412 |
. . . . . . . . . . . . . 14
⊢ 𝑐 ∈ V |
35 | 34 | snss 4699 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ ∪ 𝐴
↔ {𝑐} ⊆ ∪ 𝐴) |
36 | 33, 35 | sylibr 237 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
∧ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴)
→ 𝑐 ∈ ∪ 𝐴) |
37 | | eluni2 4823 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ ∪ 𝐴
↔ ∃𝑢 ∈
𝐴 𝑐 ∈ 𝑢) |
38 | 36, 37 | sylib 221 |
. . . . . . . . . . 11
⊢ (((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
∧ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴)
→ ∃𝑢 ∈
𝐴 𝑐 ∈ 𝑢) |
39 | | reeanv 3279 |
. . . . . . . . . . . 12
⊢
(∃𝑢 ∈
𝐴 ∃𝑤 ∈ 𝐴 (𝑐 ∈ 𝑢 ∧ 𝑏 ⊆ 𝑤) ↔ (∃𝑢 ∈ 𝐴 𝑐 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝐴 𝑏 ⊆ 𝑤)) |
40 | | simpllr 776 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
∧ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴)
∧ ((𝑢 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (𝑐 ∈ 𝑢 ∧ 𝑏 ⊆ 𝑤))) → [⊊] Or 𝐴) |
41 | | simprlr 780 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
∧ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴)
∧ ((𝑢 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (𝑐 ∈ 𝑢 ∧ 𝑏 ⊆ 𝑤))) → 𝑤 ∈ 𝐴) |
42 | | simprll 779 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
∧ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴)
∧ ((𝑢 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (𝑐 ∈ 𝑢 ∧ 𝑏 ⊆ 𝑤))) → 𝑢 ∈ 𝐴) |
43 | | sorpssun 7518 |
. . . . . . . . . . . . . . . 16
⊢ ((
[⊊] Or 𝐴
∧ (𝑤 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴)) → (𝑤 ∪ 𝑢) ∈ 𝐴) |
44 | 40, 41, 42, 43 | syl12anc 837 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
∧ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴)
∧ ((𝑢 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (𝑐 ∈ 𝑢 ∧ 𝑏 ⊆ 𝑤))) → (𝑤 ∪ 𝑢) ∈ 𝐴) |
45 | | simprrr 782 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
∧ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴)
∧ ((𝑢 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (𝑐 ∈ 𝑢 ∧ 𝑏 ⊆ 𝑤))) → 𝑏 ⊆ 𝑤) |
46 | | simprrl 781 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
∧ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴)
∧ ((𝑢 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (𝑐 ∈ 𝑢 ∧ 𝑏 ⊆ 𝑤))) → 𝑐 ∈ 𝑢) |
47 | 46 | snssd 4722 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
∧ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴)
∧ ((𝑢 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (𝑐 ∈ 𝑢 ∧ 𝑏 ⊆ 𝑤))) → {𝑐} ⊆ 𝑢) |
48 | | unss12 4096 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 ⊆ 𝑤 ∧ {𝑐} ⊆ 𝑢) → (𝑏 ∪ {𝑐}) ⊆ (𝑤 ∪ 𝑢)) |
49 | 45, 47, 48 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
∧ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴)
∧ ((𝑢 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (𝑐 ∈ 𝑢 ∧ 𝑏 ⊆ 𝑤))) → (𝑏 ∪ {𝑐}) ⊆ (𝑤 ∪ 𝑢)) |
50 | | sseq2 3927 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑤 ∪ 𝑢) → ((𝑏 ∪ {𝑐}) ⊆ 𝑧 ↔ (𝑏 ∪ {𝑐}) ⊆ (𝑤 ∪ 𝑢))) |
51 | 50 | rspcev 3537 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 ∪ 𝑢) ∈ 𝐴 ∧ (𝑏 ∪ {𝑐}) ⊆ (𝑤 ∪ 𝑢)) → ∃𝑧 ∈ 𝐴 (𝑏 ∪ {𝑐}) ⊆ 𝑧) |
52 | 44, 49, 51 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
∧ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴)
∧ ((𝑢 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (𝑐 ∈ 𝑢 ∧ 𝑏 ⊆ 𝑤))) → ∃𝑧 ∈ 𝐴 (𝑏 ∪ {𝑐}) ⊆ 𝑧) |
53 | 52 | expr 460 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
∧ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴)
∧ (𝑢 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ((𝑐 ∈ 𝑢 ∧ 𝑏 ⊆ 𝑤) → ∃𝑧 ∈ 𝐴 (𝑏 ∪ {𝑐}) ⊆ 𝑧)) |
54 | 53 | rexlimdvva 3213 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
∧ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴)
→ (∃𝑢 ∈
𝐴 ∃𝑤 ∈ 𝐴 (𝑐 ∈ 𝑢 ∧ 𝑏 ⊆ 𝑤) → ∃𝑧 ∈ 𝐴 (𝑏 ∪ {𝑐}) ⊆ 𝑧)) |
55 | 39, 54 | syl5bir 246 |
. . . . . . . . . . 11
⊢ (((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
∧ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴)
→ ((∃𝑢 ∈
𝐴 𝑐 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝐴 𝑏 ⊆ 𝑤) → ∃𝑧 ∈ 𝐴 (𝑏 ∪ {𝑐}) ⊆ 𝑧)) |
56 | 38, 55 | mpand 695 |
. . . . . . . . . 10
⊢ (((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
∧ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴)
→ (∃𝑤 ∈
𝐴 𝑏 ⊆ 𝑤 → ∃𝑧 ∈ 𝐴 (𝑏 ∪ {𝑐}) ⊆ 𝑧)) |
57 | 31, 56 | syl5bi 245 |
. . . . . . . . 9
⊢ (((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
∧ (𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴)
→ (∃𝑧 ∈
𝐴 𝑏 ⊆ 𝑧 → ∃𝑧 ∈ 𝐴 (𝑏 ∪ {𝑐}) ⊆ 𝑧)) |
58 | 57 | ex 416 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
→ ((𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴
→ (∃𝑧 ∈
𝐴 𝑏 ⊆ 𝑧 → ∃𝑧 ∈ 𝐴 (𝑏 ∪ {𝑐}) ⊆ 𝑧))) |
59 | 58 | a2d 29 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
→ (((𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴
→ ∃𝑧 ∈
𝐴 𝑏 ⊆ 𝑧) → ((𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴 → ∃𝑧 ∈ 𝐴 (𝑏 ∪ {𝑐}) ⊆ 𝑧))) |
60 | 29, 59 | syl5 34 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
→ ((𝑏 ⊆ ∪ 𝐴
→ ∃𝑧 ∈
𝐴 𝑏 ⊆ 𝑧) → ((𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴 → ∃𝑧 ∈ 𝐴 (𝑏 ∪ {𝑐}) ⊆ 𝑧))) |
61 | 60 | a2i 14 |
. . . . 5
⊢ (((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
→ (𝑏 ⊆ ∪ 𝐴
→ ∃𝑧 ∈
𝐴 𝑏 ⊆ 𝑧)) → ((𝐴 ≠ ∅ ∧ [⊊] Or
𝐴) → ((𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴 → ∃𝑧 ∈ 𝐴 (𝑏 ∪ {𝑐}) ⊆ 𝑧))) |
62 | 61 | a1i 11 |
. . . 4
⊢ (𝑏 ∈ Fin → (((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
→ (𝑏 ⊆ ∪ 𝐴
→ ∃𝑧 ∈
𝐴 𝑏 ⊆ 𝑧)) → ((𝐴 ≠ ∅ ∧ [⊊] Or
𝐴) → ((𝑏 ∪ {𝑐}) ⊆ ∪ 𝐴 → ∃𝑧 ∈ 𝐴 (𝑏 ∪ {𝑐}) ⊆ 𝑧)))) |
63 | 5, 10, 15, 20, 26, 62 | findcard2 8842 |
. . 3
⊢ (𝐵 ∈ Fin → ((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
→ (𝐵 ⊆ ∪ 𝐴
→ ∃𝑧 ∈
𝐴 𝐵 ⊆ 𝑧))) |
64 | 63 | com12 32 |
. 2
⊢ ((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
→ (𝐵 ∈ Fin →
(𝐵 ⊆ ∪ 𝐴
→ ∃𝑧 ∈
𝐴 𝐵 ⊆ 𝑧))) |
65 | 64 | imp32 422 |
1
⊢ (((𝐴 ≠ ∅ ∧
[⊊] Or 𝐴)
∧ (𝐵 ∈ Fin ∧
𝐵 ⊆ ∪ 𝐴))
→ ∃𝑧 ∈
𝐴 𝐵 ⊆ 𝑧) |