Step | Hyp | Ref
| Expression |
1 | | simpr 479 |
. . 3
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → (𝐵 ∖ 𝐶) ∈ FinII) |
2 | | simpll1 1255 |
. . . 4
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → 𝐴 ⊆ 𝒫 𝐵) |
3 | | ssel2 3739 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → 𝑔 ∈ 𝒫 𝐵) |
4 | 3 | elpwid 4314 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → 𝑔 ⊆ 𝐵) |
5 | 4 | ssdifd 3889 |
. . . . . . . 8
⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → (𝑔 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) |
6 | | sseq1 3767 |
. . . . . . . 8
⊢ (𝑓 = (𝑔 ∖ 𝐶) → (𝑓 ⊆ (𝐵 ∖ 𝐶) ↔ (𝑔 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))) |
7 | 5, 6 | syl5ibrcom 237 |
. . . . . . 7
⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → (𝑓 = (𝑔 ∖ 𝐶) → 𝑓 ⊆ (𝐵 ∖ 𝐶))) |
8 | 7 | rexlimdva 3169 |
. . . . . 6
⊢ (𝐴 ⊆ 𝒫 𝐵 → (∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶) → 𝑓 ⊆ (𝐵 ∖ 𝐶))) |
9 | | vex 3343 |
. . . . . . 7
⊢ 𝑓 ∈ V |
10 | | eqid 2760 |
. . . . . . . 8
⊢ (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) |
11 | 10 | elrnmpt 5527 |
. . . . . . 7
⊢ (𝑓 ∈ V → (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶))) |
12 | 9, 11 | ax-mp 5 |
. . . . . 6
⊢ (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶)) |
13 | | selpw 4309 |
. . . . . 6
⊢ (𝑓 ∈ 𝒫 (𝐵 ∖ 𝐶) ↔ 𝑓 ⊆ (𝐵 ∖ 𝐶)) |
14 | 8, 12, 13 | 3imtr4g 285 |
. . . . 5
⊢ (𝐴 ⊆ 𝒫 𝐵 → (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → 𝑓 ∈ 𝒫 (𝐵 ∖ 𝐶))) |
15 | 14 | ssrdv 3750 |
. . . 4
⊢ (𝐴 ⊆ 𝒫 𝐵 → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ⊆ 𝒫 (𝐵 ∖ 𝐶)) |
16 | 2, 15 | syl 17 |
. . 3
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ⊆ 𝒫 (𝐵 ∖ 𝐶)) |
17 | | simplrr 820 |
. . . 4
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → 𝐶 ∈ 𝐴) |
18 | | difid 4091 |
. . . . . . 7
⊢ (𝐶 ∖ 𝐶) = ∅ |
19 | 18 | eqcomi 2769 |
. . . . . 6
⊢ ∅ =
(𝐶 ∖ 𝐶) |
20 | | difeq1 3864 |
. . . . . . . 8
⊢ (𝑔 = 𝐶 → (𝑔 ∖ 𝐶) = (𝐶 ∖ 𝐶)) |
21 | 20 | eqeq2d 2770 |
. . . . . . 7
⊢ (𝑔 = 𝐶 → (∅ = (𝑔 ∖ 𝐶) ↔ ∅ = (𝐶 ∖ 𝐶))) |
22 | 21 | rspcev 3449 |
. . . . . 6
⊢ ((𝐶 ∈ 𝐴 ∧ ∅ = (𝐶 ∖ 𝐶)) → ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶)) |
23 | 19, 22 | mpan2 709 |
. . . . 5
⊢ (𝐶 ∈ 𝐴 → ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶)) |
24 | | 0ex 4942 |
. . . . . 6
⊢ ∅
∈ V |
25 | 10 | elrnmpt 5527 |
. . . . . 6
⊢ (∅
∈ V → (∅ ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶))) |
26 | 24, 25 | ax-mp 5 |
. . . . 5
⊢ (∅
∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶)) |
27 | 23, 26 | sylibr 224 |
. . . 4
⊢ (𝐶 ∈ 𝐴 → ∅ ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
28 | | ne0i 4064 |
. . . 4
⊢ (∅
∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ≠ ∅) |
29 | 17, 27, 28 | 3syl 18 |
. . 3
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ≠ ∅) |
30 | | simpll2 1257 |
. . . 4
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) →
[⊊] Or 𝐴) |
31 | | vex 3343 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
32 | 10 | elrnmpt 5527 |
. . . . . . . 8
⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑥 = (𝑔 ∖ 𝐶))) |
33 | 31, 32 | ax-mp 5 |
. . . . . . 7
⊢ (𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑥 = (𝑔 ∖ 𝐶)) |
34 | | difeq1 3864 |
. . . . . . . . . 10
⊢ (𝑔 = 𝑒 → (𝑔 ∖ 𝐶) = (𝑒 ∖ 𝐶)) |
35 | 34 | eqeq2d 2770 |
. . . . . . . . 9
⊢ (𝑔 = 𝑒 → (𝑥 = (𝑔 ∖ 𝐶) ↔ 𝑥 = (𝑒 ∖ 𝐶))) |
36 | 35 | cbvrexv 3311 |
. . . . . . . 8
⊢
(∃𝑔 ∈
𝐴 𝑥 = (𝑔 ∖ 𝐶) ↔ ∃𝑒 ∈ 𝐴 𝑥 = (𝑒 ∖ 𝐶)) |
37 | | sorpssi 7109 |
. . . . . . . . . . . . . . . 16
⊢ ((
[⊊] Or 𝐴
∧ (𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → (𝑒 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑒)) |
38 | | ssdif 3888 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 ⊆ 𝑔 → (𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶)) |
39 | | ssdif 3888 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 ⊆ 𝑒 → (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶)) |
40 | 38, 39 | orim12i 539 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑒 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑒) → ((𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶) ∨ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶))) |
41 | 37, 40 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((
[⊊] Or 𝐴
∧ (𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → ((𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶) ∨ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶))) |
42 | | sseq2 3768 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ↔ (𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶))) |
43 | | sseq1 3767 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑔 ∖ 𝐶) → (𝑓 ⊆ (𝑒 ∖ 𝐶) ↔ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶))) |
44 | 42, 43 | orbi12d 748 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑔 ∖ 𝐶) → (((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)) ↔ ((𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶) ∨ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶)))) |
45 | 41, 44 | syl5ibrcom 237 |
. . . . . . . . . . . . . 14
⊢ ((
[⊊] Or 𝐴
∧ (𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → (𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))) |
46 | 45 | expr 644 |
. . . . . . . . . . . . 13
⊢ ((
[⊊] Or 𝐴
∧ 𝑒 ∈ 𝐴) → (𝑔 ∈ 𝐴 → (𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))))) |
47 | 46 | rexlimdv 3168 |
. . . . . . . . . . . 12
⊢ ((
[⊊] Or 𝐴
∧ 𝑒 ∈ 𝐴) → (∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))) |
48 | 12, 47 | syl5bi 232 |
. . . . . . . . . . 11
⊢ ((
[⊊] Or 𝐴
∧ 𝑒 ∈ 𝐴) → (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))) |
49 | 48 | ralrimiv 3103 |
. . . . . . . . . 10
⊢ ((
[⊊] Or 𝐴
∧ 𝑒 ∈ 𝐴) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))) |
50 | | sseq1 3767 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑒 ∖ 𝐶) → (𝑥 ⊆ 𝑓 ↔ (𝑒 ∖ 𝐶) ⊆ 𝑓)) |
51 | | sseq2 3768 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑒 ∖ 𝐶) → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ (𝑒 ∖ 𝐶))) |
52 | 50, 51 | orbi12d 748 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑒 ∖ 𝐶) → ((𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥) ↔ ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))) |
53 | 52 | ralbidv 3124 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑒 ∖ 𝐶) → (∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥) ↔ ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))) |
54 | 49, 53 | syl5ibrcom 237 |
. . . . . . . . 9
⊢ ((
[⊊] Or 𝐴
∧ 𝑒 ∈ 𝐴) → (𝑥 = (𝑒 ∖ 𝐶) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥))) |
55 | 54 | rexlimdva 3169 |
. . . . . . . 8
⊢ (
[⊊] Or 𝐴
→ (∃𝑒 ∈
𝐴 𝑥 = (𝑒 ∖ 𝐶) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥))) |
56 | 36, 55 | syl5bi 232 |
. . . . . . 7
⊢ (
[⊊] Or 𝐴
→ (∃𝑔 ∈
𝐴 𝑥 = (𝑔 ∖ 𝐶) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥))) |
57 | 33, 56 | syl5bi 232 |
. . . . . 6
⊢ (
[⊊] Or 𝐴
→ (𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥))) |
58 | 57 | ralrimiv 3103 |
. . . . 5
⊢ (
[⊊] Or 𝐴
→ ∀𝑥 ∈ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥)) |
59 | | sorpss 7108 |
. . . . 5
⊢ (
[⊊] Or ran (𝑔
∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∀𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥)) |
60 | 58, 59 | sylibr 224 |
. . . 4
⊢ (
[⊊] Or 𝐴
→ [⊊] Or ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
61 | 30, 60 | syl 17 |
. . 3
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) →
[⊊] Or ran (𝑔
∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
62 | | fin2i 9329 |
. . 3
⊢ ((((𝐵 ∖ 𝐶) ∈ FinII ∧ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ⊆ 𝒫 (𝐵 ∖ 𝐶)) ∧ (ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ≠ ∅ ∧ [⊊] Or
ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))) → ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
63 | 1, 16, 29, 61, 62 | syl22anc 1478 |
. 2
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
64 | | simpll3 1259 |
. . 3
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → ¬
∪ 𝐴 ∈ 𝐴) |
65 | | difeq1 3864 |
. . . . . . 7
⊢ (𝑔 = 𝑓 → (𝑔 ∖ 𝐶) = (𝑓 ∖ 𝐶)) |
66 | 65 | cbvmptv 4902 |
. . . . . 6
⊢ (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∈ 𝐴 ↦ (𝑓 ∖ 𝐶)) |
67 | 66 | elrnmpt 5527 |
. . . . 5
⊢ (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → (∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑓 ∈ 𝐴 ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) |
68 | 67 | ibi 256 |
. . . 4
⊢ (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ∃𝑓 ∈ 𝐴 ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) |
69 | | eqid 2760 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ ∖ 𝐶) = (ℎ ∖ 𝐶) |
70 | | difeq1 3864 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = ℎ → (𝑔 ∖ 𝐶) = (ℎ ∖ 𝐶)) |
71 | 70 | eqeq2d 2770 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = ℎ → ((ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶) ↔ (ℎ ∖ 𝐶) = (ℎ ∖ 𝐶))) |
72 | 71 | rspcev 3449 |
. . . . . . . . . . . . . . . 16
⊢ ((ℎ ∈ 𝐴 ∧ (ℎ ∖ 𝐶) = (ℎ ∖ 𝐶)) → ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
73 | 69, 72 | mpan2 709 |
. . . . . . . . . . . . . . 15
⊢ (ℎ ∈ 𝐴 → ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
74 | 73 | adantl 473 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
75 | | vex 3343 |
. . . . . . . . . . . . . . 15
⊢ ℎ ∈ V |
76 | | difexg 4960 |
. . . . . . . . . . . . . . 15
⊢ (ℎ ∈ V → (ℎ ∖ 𝐶) ∈ V) |
77 | 10 | elrnmpt 5527 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ ∖ 𝐶) ∈ V → ((ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶))) |
78 | 75, 76, 77 | mp2b 10 |
. . . . . . . . . . . . . 14
⊢ ((ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
79 | 74, 78 | sylibr 224 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
80 | | elssuni 4619 |
. . . . . . . . . . . . 13
⊢ ((ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → (ℎ ∖ 𝐶) ⊆ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ⊆ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
82 | | simplr 809 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) |
83 | 81, 82 | sseqtrd 3782 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶)) |
84 | 83 | adantll 752 |
. . . . . . . . . 10
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶)) |
85 | | unss2 3927 |
. . . . . . . . . . 11
⊢ ((ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶) → (𝐶 ∪ (ℎ ∖ 𝐶)) ⊆ (𝐶 ∪ (𝑓 ∖ 𝐶))) |
86 | | uncom 3900 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∪ (ℎ ∖ 𝐶)) = ((ℎ ∖ 𝐶) ∪ 𝐶) |
87 | | undif1 4187 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ ∖ 𝐶) ∪ 𝐶) = (ℎ ∪ 𝐶) |
88 | 86, 87 | eqtri 2782 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∪ (ℎ ∖ 𝐶)) = (ℎ ∪ 𝐶) |
89 | 88 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝐶 ∪ (ℎ ∖ 𝐶)) = (ℎ ∪ 𝐶)) |
90 | 64 | ad2antrr 764 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ¬ ∪
𝐴 ∈ 𝐴) |
91 | 17 | ad2antrr 764 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → 𝐶 ∈ 𝐴) |
92 | | simplrr 820 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) |
93 | | eqeq1 2764 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑒 = (𝑥 ∖ 𝐶) → (𝑒 = ∅ ↔ (𝑥 ∖ 𝐶) = ∅)) |
94 | | simpllr 817 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) |
95 | | ssdif0 4085 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓 ⊆ 𝐶 ↔ (𝑓 ∖ 𝐶) = ∅) |
96 | 95 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 ⊆ 𝐶 → (𝑓 ∖ 𝐶) = ∅) |
97 | 96 | ad2antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → (𝑓 ∖ 𝐶) = ∅) |
98 | 94, 97 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = ∅) |
99 | | uni0c 4616 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = ∅ ↔ ∀𝑒 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))𝑒 = ∅) |
100 | 98, 99 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → ∀𝑒 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))𝑒 = ∅) |
101 | | eqid 2760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 ∖ 𝐶) = (𝑥 ∖ 𝐶) |
102 | | difeq1 3864 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑔 = 𝑥 → (𝑔 ∖ 𝐶) = (𝑥 ∖ 𝐶)) |
103 | 102 | eqeq2d 2770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑔 = 𝑥 → ((𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶) ↔ (𝑥 ∖ 𝐶) = (𝑥 ∖ 𝐶))) |
104 | 103 | rspcev 3449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ 𝐴 ∧ (𝑥 ∖ 𝐶) = (𝑥 ∖ 𝐶)) → ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
105 | 101, 104 | mpan2 709 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ 𝐴 → ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
106 | | difexg 4960 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 ∈ V → (𝑥 ∖ 𝐶) ∈ V) |
107 | 10 | elrnmpt 5527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∖ 𝐶) ∈ V → ((𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶))) |
108 | 31, 106, 107 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
109 | 105, 108 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ 𝐴 → (𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
110 | 109 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
111 | 93, 100, 110 | rspcdva 3455 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∖ 𝐶) = ∅) |
112 | | ssdif0 4085 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ⊆ 𝐶 ↔ (𝑥 ∖ 𝐶) = ∅) |
113 | 111, 112 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ 𝐶) |
114 | 113 | ralrimiva 3104 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐶) |
115 | | unissb 4621 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∪ 𝐴
⊆ 𝐶 ↔
∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐶) |
116 | 114, 115 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∪ 𝐴 ⊆ 𝐶) |
117 | | elssuni 4619 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐶 ∈ 𝐴 → 𝐶 ⊆ ∪ 𝐴) |
118 | 117 | ad2antrr 764 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → 𝐶 ⊆ ∪ 𝐴) |
119 | 116, 118 | eqssd 3761 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∪ 𝐴 = 𝐶) |
120 | | simpll 807 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → 𝐶 ∈ 𝐴) |
121 | 119, 120 | eqeltrd 2839 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∪ 𝐴 ∈ 𝐴) |
122 | 121 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) → (𝑓 ⊆ 𝐶 → ∪ 𝐴 ∈ 𝐴)) |
123 | 91, 92, 122 | syl2anc 696 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝑓 ⊆ 𝐶 → ∪ 𝐴 ∈ 𝐴)) |
124 | 90, 123 | mtod 189 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ¬ 𝑓 ⊆ 𝐶) |
125 | 30 | ad2antrr 764 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → [⊊] Or 𝐴) |
126 | | simplrl 819 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → 𝑓 ∈ 𝐴) |
127 | | sorpssi 7109 |
. . . . . . . . . . . . . . . 16
⊢ ((
[⊊] Or 𝐴
∧ (𝑓 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓)) |
128 | 125, 126,
91, 127 | syl12anc 1475 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓)) |
129 | | orel1 396 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑓 ⊆ 𝐶 → ((𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓) → 𝐶 ⊆ 𝑓)) |
130 | 124, 128,
129 | sylc 65 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → 𝐶 ⊆ 𝑓) |
131 | | undif 4193 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ⊆ 𝑓 ↔ (𝐶 ∪ (𝑓 ∖ 𝐶)) = 𝑓) |
132 | 130, 131 | sylib 208 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝐶 ∪ (𝑓 ∖ 𝐶)) = 𝑓) |
133 | 89, 132 | sseq12d 3775 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ((𝐶 ∪ (ℎ ∖ 𝐶)) ⊆ (𝐶 ∪ (𝑓 ∖ 𝐶)) ↔ (ℎ ∪ 𝐶) ⊆ 𝑓)) |
134 | | ssun1 3919 |
. . . . . . . . . . . . 13
⊢ ℎ ⊆ (ℎ ∪ 𝐶) |
135 | | sstr 3752 |
. . . . . . . . . . . . 13
⊢ ((ℎ ⊆ (ℎ ∪ 𝐶) ∧ (ℎ ∪ 𝐶) ⊆ 𝑓) → ℎ ⊆ 𝑓) |
136 | 134, 135 | mpan 708 |
. . . . . . . . . . . 12
⊢ ((ℎ ∪ 𝐶) ⊆ 𝑓 → ℎ ⊆ 𝑓) |
137 | 133, 136 | syl6bi 243 |
. . . . . . . . . . 11
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ((𝐶 ∪ (ℎ ∖ 𝐶)) ⊆ (𝐶 ∪ (𝑓 ∖ 𝐶)) → ℎ ⊆ 𝑓)) |
138 | 85, 137 | syl5 34 |
. . . . . . . . . 10
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ((ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶) → ℎ ⊆ 𝑓)) |
139 | 84, 138 | mpd 15 |
. . . . . . . . 9
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ℎ ⊆ 𝑓) |
140 | 139 | ralrimiva 3104 |
. . . . . . . 8
⊢
(((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∀ℎ ∈ 𝐴 ℎ ⊆ 𝑓) |
141 | | unissb 4621 |
. . . . . . . 8
⊢ (∪ 𝐴
⊆ 𝑓 ↔
∀ℎ ∈ 𝐴 ℎ ⊆ 𝑓) |
142 | 140, 141 | sylibr 224 |
. . . . . . 7
⊢
(((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∪
𝐴 ⊆ 𝑓) |
143 | | elssuni 4619 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝐴 → 𝑓 ⊆ ∪ 𝐴) |
144 | 143 | ad2antrl 766 |
. . . . . . 7
⊢
(((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → 𝑓 ⊆ ∪ 𝐴) |
145 | 142, 144 | eqssd 3761 |
. . . . . 6
⊢
(((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∪
𝐴 = 𝑓) |
146 | | simprl 811 |
. . . . . 6
⊢
(((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → 𝑓 ∈ 𝐴) |
147 | 145, 146 | eqeltrd 2839 |
. . . . 5
⊢
(((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∪
𝐴 ∈ 𝐴) |
148 | 147 | rexlimdvaa 3170 |
. . . 4
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) →
(∃𝑓 ∈ 𝐴 ∪
ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶) → ∪ 𝐴 ∈ 𝐴)) |
149 | 68, 148 | syl5 34 |
. . 3
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ∪ 𝐴 ∈ 𝐴)) |
150 | 64, 149 | mtod 189 |
. 2
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → ¬
∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
151 | 63, 150 | pm2.65da 601 |
1
⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵 ∖ 𝐶) ∈ FinII) |