Step | Hyp | Ref
| Expression |
1 | | eqneqall 2954 |
. . . 4
⊢ (𝑎 = ∅ → (𝑎 ≠ ∅ → (
[⊊] Or 𝑎
→ ∪ 𝑎 ∈ 𝑎))) |
2 | | tru 1545 |
. . . . 5
⊢
⊤ |
3 | 2 | a1i 11 |
. . . 4
⊢ (𝑎 = ∅ →
⊤) |
4 | 1, 3 | 2thd 264 |
. . 3
⊢ (𝑎 = ∅ → ((𝑎 ≠ ∅ → (
[⊊] Or 𝑎
→ ∪ 𝑎 ∈ 𝑎)) ↔ ⊤)) |
5 | | neeq1 3006 |
. . . 4
⊢ (𝑎 = 𝑏 → (𝑎 ≠ ∅ ↔ 𝑏 ≠ ∅)) |
6 | | soeq2 5567 |
. . . . 5
⊢ (𝑎 = 𝑏 → ( [⊊] Or 𝑎 ↔ [⊊] Or
𝑏)) |
7 | | unieq 4876 |
. . . . . 6
⊢ (𝑎 = 𝑏 → ∪ 𝑎 = ∪
𝑏) |
8 | | id 22 |
. . . . . 6
⊢ (𝑎 = 𝑏 → 𝑎 = 𝑏) |
9 | 7, 8 | eleq12d 2832 |
. . . . 5
⊢ (𝑎 = 𝑏 → (∪ 𝑎 ∈ 𝑎 ↔ ∪ 𝑏 ∈ 𝑏)) |
10 | 6, 9 | imbi12d 344 |
. . . 4
⊢ (𝑎 = 𝑏 → (( [⊊] Or 𝑎 → ∪ 𝑎
∈ 𝑎) ↔ (
[⊊] Or 𝑏
→ ∪ 𝑏 ∈ 𝑏))) |
11 | 5, 10 | imbi12d 344 |
. . 3
⊢ (𝑎 = 𝑏 → ((𝑎 ≠ ∅ → ( [⊊] Or
𝑎 → ∪ 𝑎
∈ 𝑎)) ↔ (𝑏 ≠ ∅ → (
[⊊] Or 𝑏
→ ∪ 𝑏 ∈ 𝑏)))) |
12 | | neeq1 3006 |
. . . 4
⊢ (𝑎 = (𝑏 ∪ {𝑐}) → (𝑎 ≠ ∅ ↔ (𝑏 ∪ {𝑐}) ≠ ∅)) |
13 | | soeq2 5567 |
. . . . 5
⊢ (𝑎 = (𝑏 ∪ {𝑐}) → ( [⊊] Or 𝑎 ↔ [⊊] Or
(𝑏 ∪ {𝑐}))) |
14 | | unieq 4876 |
. . . . . 6
⊢ (𝑎 = (𝑏 ∪ {𝑐}) → ∪ 𝑎 = ∪
(𝑏 ∪ {𝑐})) |
15 | | id 22 |
. . . . . 6
⊢ (𝑎 = (𝑏 ∪ {𝑐}) → 𝑎 = (𝑏 ∪ {𝑐})) |
16 | 14, 15 | eleq12d 2832 |
. . . . 5
⊢ (𝑎 = (𝑏 ∪ {𝑐}) → (∪ 𝑎 ∈ 𝑎 ↔ ∪ (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))) |
17 | 13, 16 | imbi12d 344 |
. . . 4
⊢ (𝑎 = (𝑏 ∪ {𝑐}) → (( [⊊] Or 𝑎 → ∪ 𝑎
∈ 𝑎) ↔ (
[⊊] Or (𝑏
∪ {𝑐}) → ∪ (𝑏
∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})))) |
18 | 12, 17 | imbi12d 344 |
. . 3
⊢ (𝑎 = (𝑏 ∪ {𝑐}) → ((𝑎 ≠ ∅ → ( [⊊] Or
𝑎 → ∪ 𝑎
∈ 𝑎)) ↔ ((𝑏 ∪ {𝑐}) ≠ ∅ → ( [⊊] Or
(𝑏 ∪ {𝑐}) → ∪ (𝑏
∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))))) |
19 | | neeq1 3006 |
. . . 4
⊢ (𝑎 = 𝐴 → (𝑎 ≠ ∅ ↔ 𝐴 ≠ ∅)) |
20 | | soeq2 5567 |
. . . . 5
⊢ (𝑎 = 𝐴 → ( [⊊] Or 𝑎 ↔ [⊊] Or
𝐴)) |
21 | | unieq 4876 |
. . . . . 6
⊢ (𝑎 = 𝐴 → ∪ 𝑎 = ∪
𝐴) |
22 | | id 22 |
. . . . . 6
⊢ (𝑎 = 𝐴 → 𝑎 = 𝐴) |
23 | 21, 22 | eleq12d 2832 |
. . . . 5
⊢ (𝑎 = 𝐴 → (∪ 𝑎 ∈ 𝑎 ↔ ∪ 𝐴 ∈ 𝐴)) |
24 | 20, 23 | imbi12d 344 |
. . . 4
⊢ (𝑎 = 𝐴 → (( [⊊] Or 𝑎 → ∪ 𝑎
∈ 𝑎) ↔ (
[⊊] Or 𝐴
→ ∪ 𝐴 ∈ 𝐴))) |
25 | 19, 24 | imbi12d 344 |
. . 3
⊢ (𝑎 = 𝐴 → ((𝑎 ≠ ∅ → ( [⊊] Or
𝑎 → ∪ 𝑎
∈ 𝑎)) ↔ (𝐴 ≠ ∅ → (
[⊊] Or 𝐴
→ ∪ 𝐴 ∈ 𝐴)))) |
26 | | unisnv 4888 |
. . . . . . . . . 10
⊢ ∪ {𝑐}
= 𝑐 |
27 | | vsnid 4623 |
. . . . . . . . . 10
⊢ 𝑐 ∈ {𝑐} |
28 | 26, 27 | eqeltri 2834 |
. . . . . . . . 9
⊢ ∪ {𝑐}
∈ {𝑐} |
29 | | uneq1 4116 |
. . . . . . . . . . . 12
⊢ (𝑏 = ∅ → (𝑏 ∪ {𝑐}) = (∅ ∪ {𝑐})) |
30 | | uncom 4113 |
. . . . . . . . . . . . 13
⊢ (∅
∪ {𝑐}) = ({𝑐} ∪
∅) |
31 | | un0 4350 |
. . . . . . . . . . . . 13
⊢ ({𝑐} ∪ ∅) = {𝑐} |
32 | 30, 31 | eqtri 2764 |
. . . . . . . . . . . 12
⊢ (∅
∪ {𝑐}) = {𝑐} |
33 | 29, 32 | eqtrdi 2792 |
. . . . . . . . . . 11
⊢ (𝑏 = ∅ → (𝑏 ∪ {𝑐}) = {𝑐}) |
34 | 33 | unieqd 4879 |
. . . . . . . . . 10
⊢ (𝑏 = ∅ → ∪ (𝑏
∪ {𝑐}) = ∪ {𝑐}) |
35 | 34, 33 | eleq12d 2832 |
. . . . . . . . 9
⊢ (𝑏 = ∅ → (∪ (𝑏
∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}) ↔ ∪ {𝑐} ∈ {𝑐})) |
36 | 28, 35 | mpbiri 257 |
. . . . . . . 8
⊢ (𝑏 = ∅ → ∪ (𝑏
∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})) |
37 | 36 | a1d 25 |
. . . . . . 7
⊢ (𝑏 = ∅ → ((𝑏 ≠ ∅ → (
[⊊] Or 𝑏
→ ∪ 𝑏 ∈ 𝑏)) → ∪ (𝑏 ∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))) |
38 | 37 | adantl 482 |
. . . . . 6
⊢ (((𝑏 ∈ Fin ∧
[⊊] Or (𝑏
∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 = ∅) → ((𝑏 ≠ ∅ → ( [⊊] Or
𝑏 → ∪ 𝑏
∈ 𝑏)) → ∪ (𝑏
∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))) |
39 | | simpr 485 |
. . . . . . 7
⊢ (((𝑏 ∈ Fin ∧
[⊊] Or (𝑏
∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → 𝑏 ≠ ∅) |
40 | | ssun1 4132 |
. . . . . . . . 9
⊢ 𝑏 ⊆ (𝑏 ∪ {𝑐}) |
41 | | simpl2 1192 |
. . . . . . . . 9
⊢ (((𝑏 ∈ Fin ∧
[⊊] Or (𝑏
∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → [⊊] Or
(𝑏 ∪ {𝑐})) |
42 | | soss 5565 |
. . . . . . . . 9
⊢ (𝑏 ⊆ (𝑏 ∪ {𝑐}) → ( [⊊] Or (𝑏 ∪ {𝑐}) → [⊊] Or 𝑏)) |
43 | 40, 41, 42 | mpsyl 68 |
. . . . . . . 8
⊢ (((𝑏 ∈ Fin ∧
[⊊] Or (𝑏
∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → [⊊] Or
𝑏) |
44 | | uniun 4891 |
. . . . . . . . . . 11
⊢ ∪ (𝑏
∪ {𝑐}) = (∪ 𝑏
∪ ∪ {𝑐}) |
45 | 26 | uneq2i 4120 |
. . . . . . . . . . 11
⊢ (∪ 𝑏
∪ ∪ {𝑐}) = (∪ 𝑏 ∪ 𝑐) |
46 | 44, 45 | eqtri 2764 |
. . . . . . . . . 10
⊢ ∪ (𝑏
∪ {𝑐}) = (∪ 𝑏
∪ 𝑐) |
47 | | simprr 771 |
. . . . . . . . . . 11
⊢ (((𝑏 ∈ Fin ∧
[⊊] Or (𝑏
∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ ∪ 𝑏
∈ 𝑏)) → ∪ 𝑏
∈ 𝑏) |
48 | | simpl2 1192 |
. . . . . . . . . . . 12
⊢ (((𝑏 ∈ Fin ∧
[⊊] Or (𝑏
∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ ∪ 𝑏
∈ 𝑏)) →
[⊊] Or (𝑏
∪ {𝑐})) |
49 | | elun1 4136 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑏
∈ 𝑏 → ∪ 𝑏
∈ (𝑏 ∪ {𝑐})) |
50 | 49 | ad2antll 727 |
. . . . . . . . . . . 12
⊢ (((𝑏 ∈ Fin ∧
[⊊] Or (𝑏
∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ ∪ 𝑏
∈ 𝑏)) → ∪ 𝑏
∈ (𝑏 ∪ {𝑐})) |
51 | | ssun2 4133 |
. . . . . . . . . . . . . 14
⊢ {𝑐} ⊆ (𝑏 ∪ {𝑐}) |
52 | 51, 27 | sselii 3941 |
. . . . . . . . . . . . 13
⊢ 𝑐 ∈ (𝑏 ∪ {𝑐}) |
53 | 52 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑏 ∈ Fin ∧
[⊊] Or (𝑏
∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ ∪ 𝑏
∈ 𝑏)) → 𝑐 ∈ (𝑏 ∪ {𝑐})) |
54 | | sorpssi 7666 |
. . . . . . . . . . . 12
⊢ ((
[⊊] Or (𝑏
∪ {𝑐}) ∧ (∪ 𝑏
∈ (𝑏 ∪ {𝑐}) ∧ 𝑐 ∈ (𝑏 ∪ {𝑐}))) → (∪
𝑏 ⊆ 𝑐 ∨ 𝑐 ⊆ ∪ 𝑏)) |
55 | 48, 50, 53, 54 | syl12anc 835 |
. . . . . . . . . . 11
⊢ (((𝑏 ∈ Fin ∧
[⊊] Or (𝑏
∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ ∪ 𝑏
∈ 𝑏)) → (∪ 𝑏
⊆ 𝑐 ∨ 𝑐 ⊆ ∪ 𝑏)) |
56 | | ssequn1 4140 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑏
⊆ 𝑐 ↔ (∪ 𝑏
∪ 𝑐) = 𝑐) |
57 | 52 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (∪ 𝑏
∈ 𝑏 → 𝑐 ∈ (𝑏 ∪ {𝑐})) |
58 | | eleq1 2825 |
. . . . . . . . . . . . . . 15
⊢ ((∪ 𝑏
∪ 𝑐) = 𝑐 → ((∪ 𝑏
∪ 𝑐) ∈ (𝑏 ∪ {𝑐}) ↔ 𝑐 ∈ (𝑏 ∪ {𝑐}))) |
59 | 57, 58 | syl5ibr 245 |
. . . . . . . . . . . . . 14
⊢ ((∪ 𝑏
∪ 𝑐) = 𝑐 → (∪ 𝑏
∈ 𝑏 → (∪ 𝑏
∪ 𝑐) ∈ (𝑏 ∪ {𝑐}))) |
60 | 56, 59 | sylbi 216 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑏
⊆ 𝑐 → (∪ 𝑏
∈ 𝑏 → (∪ 𝑏
∪ 𝑐) ∈ (𝑏 ∪ {𝑐}))) |
61 | 60 | impcom 408 |
. . . . . . . . . . . 12
⊢ ((∪ 𝑏
∈ 𝑏 ∧ ∪ 𝑏
⊆ 𝑐) → (∪ 𝑏
∪ 𝑐) ∈ (𝑏 ∪ {𝑐})) |
62 | | uncom 4113 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑏
∪ 𝑐) = (𝑐 ∪ ∪ 𝑏) |
63 | | ssequn1 4140 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ⊆ ∪ 𝑏
↔ (𝑐 ∪ ∪ 𝑏) =
∪ 𝑏) |
64 | | eleq1 2825 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 ∪ ∪ 𝑏) =
∪ 𝑏 → ((𝑐 ∪ ∪ 𝑏) ∈ (𝑏 ∪ {𝑐}) ↔ ∪ 𝑏 ∈ (𝑏 ∪ {𝑐}))) |
65 | 49, 64 | syl5ibr 245 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 ∪ ∪ 𝑏) =
∪ 𝑏 → (∪ 𝑏 ∈ 𝑏 → (𝑐 ∪ ∪ 𝑏) ∈ (𝑏 ∪ {𝑐}))) |
66 | 63, 65 | sylbi 216 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ⊆ ∪ 𝑏
→ (∪ 𝑏 ∈ 𝑏 → (𝑐 ∪ ∪ 𝑏) ∈ (𝑏 ∪ {𝑐}))) |
67 | 66 | impcom 408 |
. . . . . . . . . . . . 13
⊢ ((∪ 𝑏
∈ 𝑏 ∧ 𝑐 ⊆ ∪ 𝑏)
→ (𝑐 ∪ ∪ 𝑏)
∈ (𝑏 ∪ {𝑐})) |
68 | 62, 67 | eqeltrid 2842 |
. . . . . . . . . . . 12
⊢ ((∪ 𝑏
∈ 𝑏 ∧ 𝑐 ⊆ ∪ 𝑏)
→ (∪ 𝑏 ∪ 𝑐) ∈ (𝑏 ∪ {𝑐})) |
69 | 61, 68 | jaodan 956 |
. . . . . . . . . . 11
⊢ ((∪ 𝑏
∈ 𝑏 ∧ (∪ 𝑏
⊆ 𝑐 ∨ 𝑐 ⊆ ∪ 𝑏))
→ (∪ 𝑏 ∪ 𝑐) ∈ (𝑏 ∪ {𝑐})) |
70 | 47, 55, 69 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝑏 ∈ Fin ∧
[⊊] Or (𝑏
∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ ∪ 𝑏
∈ 𝑏)) → (∪ 𝑏
∪ 𝑐) ∈ (𝑏 ∪ {𝑐})) |
71 | 46, 70 | eqeltrid 2842 |
. . . . . . . . 9
⊢ (((𝑏 ∈ Fin ∧
[⊊] Or (𝑏
∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ (𝑏 ≠ ∅ ∧ ∪ 𝑏
∈ 𝑏)) → ∪ (𝑏
∪ {𝑐}) ∈ (𝑏 ∪ {𝑐})) |
72 | 71 | expr 457 |
. . . . . . . 8
⊢ (((𝑏 ∈ Fin ∧
[⊊] Or (𝑏
∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → (∪ 𝑏
∈ 𝑏 → ∪ (𝑏
∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))) |
73 | 43, 72 | embantd 59 |
. . . . . . 7
⊢ (((𝑏 ∈ Fin ∧
[⊊] Or (𝑏
∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → (( [⊊] Or
𝑏 → ∪ 𝑏
∈ 𝑏) → ∪ (𝑏
∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))) |
74 | 39, 73 | embantd 59 |
. . . . . 6
⊢ (((𝑏 ∈ Fin ∧
[⊊] Or (𝑏
∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) ∧ 𝑏 ≠ ∅) → ((𝑏 ≠ ∅ → ( [⊊] Or
𝑏 → ∪ 𝑏
∈ 𝑏)) → ∪ (𝑏
∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))) |
75 | 38, 74 | pm2.61dane 3032 |
. . . . 5
⊢ ((𝑏 ∈ Fin ∧
[⊊] Or (𝑏
∪ {𝑐}) ∧ (𝑏 ∪ {𝑐}) ≠ ∅) → ((𝑏 ≠ ∅ → ( [⊊] Or
𝑏 → ∪ 𝑏
∈ 𝑏)) → ∪ (𝑏
∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))) |
76 | 75 | 3exp 1119 |
. . . 4
⊢ (𝑏 ∈ Fin → (
[⊊] Or (𝑏
∪ {𝑐}) → ((𝑏 ∪ {𝑐}) ≠ ∅ → ((𝑏 ≠ ∅ → ( [⊊] Or
𝑏 → ∪ 𝑏
∈ 𝑏)) → ∪ (𝑏
∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))))) |
77 | 76 | com24 95 |
. . 3
⊢ (𝑏 ∈ Fin → ((𝑏 ≠ ∅ → (
[⊊] Or 𝑏
→ ∪ 𝑏 ∈ 𝑏)) → ((𝑏 ∪ {𝑐}) ≠ ∅ → ( [⊊] Or
(𝑏 ∪ {𝑐}) → ∪ (𝑏
∪ {𝑐}) ∈ (𝑏 ∪ {𝑐}))))) |
78 | 4, 11, 18, 25, 2, 77 | findcard2 9108 |
. 2
⊢ (𝐴 ∈ Fin → (𝐴 ≠ ∅ → (
[⊊] Or 𝐴
→ ∪ 𝐴 ∈ 𝐴))) |
79 | 78 | 3imp21 1114 |
1
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ∧
[⊊] Or 𝐴)
→ ∪ 𝐴 ∈ 𝐴) |