Step | Hyp | Ref
| Expression |
1 | | simpr 488 |
. . 3
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → (𝐵 ∖ 𝐶) ∈ FinII) |
2 | | simpll1 1214 |
. . . 4
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → 𝐴 ⊆ 𝒫 𝐵) |
3 | | ssel2 3895 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → 𝑔 ∈ 𝒫 𝐵) |
4 | 3 | elpwid 4524 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → 𝑔 ⊆ 𝐵) |
5 | 4 | ssdifd 4055 |
. . . . . . . 8
⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → (𝑔 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) |
6 | | sseq1 3926 |
. . . . . . . 8
⊢ (𝑓 = (𝑔 ∖ 𝐶) → (𝑓 ⊆ (𝐵 ∖ 𝐶) ↔ (𝑔 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))) |
7 | 5, 6 | syl5ibrcom 250 |
. . . . . . 7
⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → (𝑓 = (𝑔 ∖ 𝐶) → 𝑓 ⊆ (𝐵 ∖ 𝐶))) |
8 | 7 | rexlimdva 3203 |
. . . . . 6
⊢ (𝐴 ⊆ 𝒫 𝐵 → (∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶) → 𝑓 ⊆ (𝐵 ∖ 𝐶))) |
9 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) |
10 | 9 | elrnmpt 5825 |
. . . . . . 7
⊢ (𝑓 ∈ V → (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶))) |
11 | 10 | elv 3414 |
. . . . . 6
⊢ (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶)) |
12 | | velpw 4518 |
. . . . . 6
⊢ (𝑓 ∈ 𝒫 (𝐵 ∖ 𝐶) ↔ 𝑓 ⊆ (𝐵 ∖ 𝐶)) |
13 | 8, 11, 12 | 3imtr4g 299 |
. . . . 5
⊢ (𝐴 ⊆ 𝒫 𝐵 → (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → 𝑓 ∈ 𝒫 (𝐵 ∖ 𝐶))) |
14 | 13 | ssrdv 3907 |
. . . 4
⊢ (𝐴 ⊆ 𝒫 𝐵 → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ⊆ 𝒫 (𝐵 ∖ 𝐶)) |
15 | 2, 14 | syl 17 |
. . 3
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ⊆ 𝒫 (𝐵 ∖ 𝐶)) |
16 | | simplrr 778 |
. . . 4
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → 𝐶 ∈ 𝐴) |
17 | | difid 4285 |
. . . . . . 7
⊢ (𝐶 ∖ 𝐶) = ∅ |
18 | 17 | eqcomi 2746 |
. . . . . 6
⊢ ∅ =
(𝐶 ∖ 𝐶) |
19 | | difeq1 4030 |
. . . . . . 7
⊢ (𝑔 = 𝐶 → (𝑔 ∖ 𝐶) = (𝐶 ∖ 𝐶)) |
20 | 19 | rspceeqv 3552 |
. . . . . 6
⊢ ((𝐶 ∈ 𝐴 ∧ ∅ = (𝐶 ∖ 𝐶)) → ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶)) |
21 | 18, 20 | mpan2 691 |
. . . . 5
⊢ (𝐶 ∈ 𝐴 → ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶)) |
22 | | 0ex 5200 |
. . . . . 6
⊢ ∅
∈ V |
23 | 9 | elrnmpt 5825 |
. . . . . 6
⊢ (∅
∈ V → (∅ ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶))) |
24 | 22, 23 | ax-mp 5 |
. . . . 5
⊢ (∅
∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶)) |
25 | 21, 24 | sylibr 237 |
. . . 4
⊢ (𝐶 ∈ 𝐴 → ∅ ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
26 | | ne0i 4249 |
. . . 4
⊢ (∅
∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ≠ ∅) |
27 | 16, 25, 26 | 3syl 18 |
. . 3
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ≠ ∅) |
28 | | simpll2 1215 |
. . . 4
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) →
[⊊] Or 𝐴) |
29 | 9 | elrnmpt 5825 |
. . . . . . . 8
⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑥 = (𝑔 ∖ 𝐶))) |
30 | 29 | elv 3414 |
. . . . . . 7
⊢ (𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑥 = (𝑔 ∖ 𝐶)) |
31 | | difeq1 4030 |
. . . . . . . . . 10
⊢ (𝑔 = 𝑒 → (𝑔 ∖ 𝐶) = (𝑒 ∖ 𝐶)) |
32 | 31 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑔 = 𝑒 → (𝑥 = (𝑔 ∖ 𝐶) ↔ 𝑥 = (𝑒 ∖ 𝐶))) |
33 | 32 | cbvrexvw 3359 |
. . . . . . . 8
⊢
(∃𝑔 ∈
𝐴 𝑥 = (𝑔 ∖ 𝐶) ↔ ∃𝑒 ∈ 𝐴 𝑥 = (𝑒 ∖ 𝐶)) |
34 | | sorpssi 7517 |
. . . . . . . . . . . . . . . 16
⊢ ((
[⊊] Or 𝐴
∧ (𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → (𝑒 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑒)) |
35 | | ssdif 4054 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 ⊆ 𝑔 → (𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶)) |
36 | | ssdif 4054 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 ⊆ 𝑒 → (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶)) |
37 | 35, 36 | orim12i 909 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑒 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑒) → ((𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶) ∨ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶))) |
38 | 34, 37 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((
[⊊] Or 𝐴
∧ (𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → ((𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶) ∨ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶))) |
39 | | sseq2 3927 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ↔ (𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶))) |
40 | | sseq1 3926 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑔 ∖ 𝐶) → (𝑓 ⊆ (𝑒 ∖ 𝐶) ↔ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶))) |
41 | 39, 40 | orbi12d 919 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑔 ∖ 𝐶) → (((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)) ↔ ((𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶) ∨ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶)))) |
42 | 38, 41 | syl5ibrcom 250 |
. . . . . . . . . . . . . 14
⊢ ((
[⊊] Or 𝐴
∧ (𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → (𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))) |
43 | 42 | expr 460 |
. . . . . . . . . . . . 13
⊢ ((
[⊊] Or 𝐴
∧ 𝑒 ∈ 𝐴) → (𝑔 ∈ 𝐴 → (𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))))) |
44 | 43 | rexlimdv 3202 |
. . . . . . . . . . . 12
⊢ ((
[⊊] Or 𝐴
∧ 𝑒 ∈ 𝐴) → (∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))) |
45 | 11, 44 | syl5bi 245 |
. . . . . . . . . . 11
⊢ ((
[⊊] Or 𝐴
∧ 𝑒 ∈ 𝐴) → (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))) |
46 | 45 | ralrimiv 3104 |
. . . . . . . . . 10
⊢ ((
[⊊] Or 𝐴
∧ 𝑒 ∈ 𝐴) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))) |
47 | | sseq1 3926 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑒 ∖ 𝐶) → (𝑥 ⊆ 𝑓 ↔ (𝑒 ∖ 𝐶) ⊆ 𝑓)) |
48 | | sseq2 3927 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑒 ∖ 𝐶) → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ (𝑒 ∖ 𝐶))) |
49 | 47, 48 | orbi12d 919 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑒 ∖ 𝐶) → ((𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥) ↔ ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))) |
50 | 49 | ralbidv 3118 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑒 ∖ 𝐶) → (∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥) ↔ ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))) |
51 | 46, 50 | syl5ibrcom 250 |
. . . . . . . . 9
⊢ ((
[⊊] Or 𝐴
∧ 𝑒 ∈ 𝐴) → (𝑥 = (𝑒 ∖ 𝐶) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥))) |
52 | 51 | rexlimdva 3203 |
. . . . . . . 8
⊢ (
[⊊] Or 𝐴
→ (∃𝑒 ∈
𝐴 𝑥 = (𝑒 ∖ 𝐶) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥))) |
53 | 33, 52 | syl5bi 245 |
. . . . . . 7
⊢ (
[⊊] Or 𝐴
→ (∃𝑔 ∈
𝐴 𝑥 = (𝑔 ∖ 𝐶) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥))) |
54 | 30, 53 | syl5bi 245 |
. . . . . 6
⊢ (
[⊊] Or 𝐴
→ (𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥))) |
55 | 54 | ralrimiv 3104 |
. . . . 5
⊢ (
[⊊] Or 𝐴
→ ∀𝑥 ∈ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥)) |
56 | | sorpss 7516 |
. . . . 5
⊢ (
[⊊] Or ran (𝑔
∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∀𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥)) |
57 | 55, 56 | sylibr 237 |
. . . 4
⊢ (
[⊊] Or 𝐴
→ [⊊] Or ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
58 | 28, 57 | syl 17 |
. . 3
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) →
[⊊] Or ran (𝑔
∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
59 | | fin2i 9909 |
. . 3
⊢ ((((𝐵 ∖ 𝐶) ∈ FinII ∧ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ⊆ 𝒫 (𝐵 ∖ 𝐶)) ∧ (ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ≠ ∅ ∧ [⊊] Or
ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))) → ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
60 | 1, 15, 27, 58, 59 | syl22anc 839 |
. 2
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
61 | | simpll3 1216 |
. . 3
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → ¬
∪ 𝐴 ∈ 𝐴) |
62 | | difeq1 4030 |
. . . . . . 7
⊢ (𝑔 = 𝑓 → (𝑔 ∖ 𝐶) = (𝑓 ∖ 𝐶)) |
63 | 62 | cbvmptv 5158 |
. . . . . 6
⊢ (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∈ 𝐴 ↦ (𝑓 ∖ 𝐶)) |
64 | 63 | elrnmpt 5825 |
. . . . 5
⊢ (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → (∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑓 ∈ 𝐴 ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) |
65 | 64 | ibi 270 |
. . . 4
⊢ (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ∃𝑓 ∈ 𝐴 ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) |
66 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ ∖ 𝐶) = (ℎ ∖ 𝐶) |
67 | | difeq1 4030 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = ℎ → (𝑔 ∖ 𝐶) = (ℎ ∖ 𝐶)) |
68 | 67 | rspceeqv 3552 |
. . . . . . . . . . . . . . . 16
⊢ ((ℎ ∈ 𝐴 ∧ (ℎ ∖ 𝐶) = (ℎ ∖ 𝐶)) → ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
69 | 66, 68 | mpan2 691 |
. . . . . . . . . . . . . . 15
⊢ (ℎ ∈ 𝐴 → ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
70 | 69 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
71 | | vex 3412 |
. . . . . . . . . . . . . . 15
⊢ ℎ ∈ V |
72 | | difexg 5220 |
. . . . . . . . . . . . . . 15
⊢ (ℎ ∈ V → (ℎ ∖ 𝐶) ∈ V) |
73 | 9 | elrnmpt 5825 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ ∖ 𝐶) ∈ V → ((ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶))) |
74 | 71, 72, 73 | mp2b 10 |
. . . . . . . . . . . . . 14
⊢ ((ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
75 | 70, 74 | sylibr 237 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
76 | | elssuni 4851 |
. . . . . . . . . . . . 13
⊢ ((ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → (ℎ ∖ 𝐶) ⊆ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ⊆ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
78 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) |
79 | 77, 78 | sseqtrd 3941 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶)) |
80 | 79 | adantll 714 |
. . . . . . . . . 10
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶)) |
81 | | unss2 4095 |
. . . . . . . . . . 11
⊢ ((ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶) → (𝐶 ∪ (ℎ ∖ 𝐶)) ⊆ (𝐶 ∪ (𝑓 ∖ 𝐶))) |
82 | | uncom 4067 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∪ (ℎ ∖ 𝐶)) = ((ℎ ∖ 𝐶) ∪ 𝐶) |
83 | | undif1 4390 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ ∖ 𝐶) ∪ 𝐶) = (ℎ ∪ 𝐶) |
84 | 82, 83 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∪ (ℎ ∖ 𝐶)) = (ℎ ∪ 𝐶) |
85 | 84 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝐶 ∪ (ℎ ∖ 𝐶)) = (ℎ ∪ 𝐶)) |
86 | 61 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ¬ ∪
𝐴 ∈ 𝐴) |
87 | 16 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → 𝐶 ∈ 𝐴) |
88 | | simplrr 778 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) |
89 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑒 = (𝑥 ∖ 𝐶) → (𝑒 = ∅ ↔ (𝑥 ∖ 𝐶) = ∅)) |
90 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) |
91 | | ssdif0 4278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓 ⊆ 𝐶 ↔ (𝑓 ∖ 𝐶) = ∅) |
92 | 91 | biimpi 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 ⊆ 𝐶 → (𝑓 ∖ 𝐶) = ∅) |
93 | 92 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → (𝑓 ∖ 𝐶) = ∅) |
94 | 90, 93 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = ∅) |
95 | | uni0c 4848 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = ∅ ↔ ∀𝑒 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))𝑒 = ∅) |
96 | 94, 95 | sylib 221 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → ∀𝑒 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))𝑒 = ∅) |
97 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 ∖ 𝐶) = (𝑥 ∖ 𝐶) |
98 | | difeq1 4030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑔 = 𝑥 → (𝑔 ∖ 𝐶) = (𝑥 ∖ 𝐶)) |
99 | 98 | rspceeqv 3552 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ 𝐴 ∧ (𝑥 ∖ 𝐶) = (𝑥 ∖ 𝐶)) → ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
100 | 97, 99 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ 𝐴 → ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
101 | | vex 3412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑥 ∈ V |
102 | | difexg 5220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 ∈ V → (𝑥 ∖ 𝐶) ∈ V) |
103 | 9 | elrnmpt 5825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∖ 𝐶) ∈ V → ((𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶))) |
104 | 101, 102,
103 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
105 | 100, 104 | sylibr 237 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ 𝐴 → (𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
106 | 105 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
107 | 89, 96, 106 | rspcdva 3539 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∖ 𝐶) = ∅) |
108 | | ssdif0 4278 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ⊆ 𝐶 ↔ (𝑥 ∖ 𝐶) = ∅) |
109 | 107, 108 | sylibr 237 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ 𝐶) |
110 | 109 | ralrimiva 3105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐶) |
111 | | unissb 4853 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∪ 𝐴
⊆ 𝐶 ↔
∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐶) |
112 | 110, 111 | sylibr 237 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∪ 𝐴 ⊆ 𝐶) |
113 | | elssuni 4851 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐶 ∈ 𝐴 → 𝐶 ⊆ ∪ 𝐴) |
114 | 113 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → 𝐶 ⊆ ∪ 𝐴) |
115 | 112, 114 | eqssd 3918 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∪ 𝐴 = 𝐶) |
116 | | simpll 767 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → 𝐶 ∈ 𝐴) |
117 | 115, 116 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∪ 𝐴 ∈ 𝐴) |
118 | 117 | ex 416 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) → (𝑓 ⊆ 𝐶 → ∪ 𝐴 ∈ 𝐴)) |
119 | 87, 88, 118 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝑓 ⊆ 𝐶 → ∪ 𝐴 ∈ 𝐴)) |
120 | 86, 119 | mtod 201 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ¬ 𝑓 ⊆ 𝐶) |
121 | 28 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → [⊊] Or 𝐴) |
122 | | simplrl 777 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → 𝑓 ∈ 𝐴) |
123 | | sorpssi 7517 |
. . . . . . . . . . . . . . . 16
⊢ ((
[⊊] Or 𝐴
∧ (𝑓 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓)) |
124 | 121, 122,
87, 123 | syl12anc 837 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓)) |
125 | | orel1 889 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑓 ⊆ 𝐶 → ((𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓) → 𝐶 ⊆ 𝑓)) |
126 | 120, 124,
125 | sylc 65 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → 𝐶 ⊆ 𝑓) |
127 | | undif 4396 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ⊆ 𝑓 ↔ (𝐶 ∪ (𝑓 ∖ 𝐶)) = 𝑓) |
128 | 126, 127 | sylib 221 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝐶 ∪ (𝑓 ∖ 𝐶)) = 𝑓) |
129 | 85, 128 | sseq12d 3934 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ((𝐶 ∪ (ℎ ∖ 𝐶)) ⊆ (𝐶 ∪ (𝑓 ∖ 𝐶)) ↔ (ℎ ∪ 𝐶) ⊆ 𝑓)) |
130 | | ssun1 4086 |
. . . . . . . . . . . . 13
⊢ ℎ ⊆ (ℎ ∪ 𝐶) |
131 | | sstr 3909 |
. . . . . . . . . . . . 13
⊢ ((ℎ ⊆ (ℎ ∪ 𝐶) ∧ (ℎ ∪ 𝐶) ⊆ 𝑓) → ℎ ⊆ 𝑓) |
132 | 130, 131 | mpan 690 |
. . . . . . . . . . . 12
⊢ ((ℎ ∪ 𝐶) ⊆ 𝑓 → ℎ ⊆ 𝑓) |
133 | 129, 132 | syl6bi 256 |
. . . . . . . . . . 11
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ((𝐶 ∪ (ℎ ∖ 𝐶)) ⊆ (𝐶 ∪ (𝑓 ∖ 𝐶)) → ℎ ⊆ 𝑓)) |
134 | 81, 133 | syl5 34 |
. . . . . . . . . 10
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ((ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶) → ℎ ⊆ 𝑓)) |
135 | 80, 134 | mpd 15 |
. . . . . . . . 9
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ℎ ⊆ 𝑓) |
136 | 135 | ralrimiva 3105 |
. . . . . . . 8
⊢
(((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∀ℎ ∈ 𝐴 ℎ ⊆ 𝑓) |
137 | | unissb 4853 |
. . . . . . . 8
⊢ (∪ 𝐴
⊆ 𝑓 ↔
∀ℎ ∈ 𝐴 ℎ ⊆ 𝑓) |
138 | 136, 137 | sylibr 237 |
. . . . . . 7
⊢
(((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∪
𝐴 ⊆ 𝑓) |
139 | | elssuni 4851 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝐴 → 𝑓 ⊆ ∪ 𝐴) |
140 | 139 | ad2antrl 728 |
. . . . . . 7
⊢
(((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → 𝑓 ⊆ ∪ 𝐴) |
141 | 138, 140 | eqssd 3918 |
. . . . . 6
⊢
(((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∪
𝐴 = 𝑓) |
142 | | simprl 771 |
. . . . . 6
⊢
(((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → 𝑓 ∈ 𝐴) |
143 | 141, 142 | eqeltrd 2838 |
. . . . 5
⊢
(((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∪
𝐴 ∈ 𝐴) |
144 | 143 | rexlimdvaa 3204 |
. . . 4
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) →
(∃𝑓 ∈ 𝐴 ∪
ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶) → ∪ 𝐴 ∈ 𝐴)) |
145 | 65, 144 | syl5 34 |
. . 3
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ∪ 𝐴 ∈ 𝐴)) |
146 | 61, 145 | mtod 201 |
. 2
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → ¬
∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
147 | 60, 146 | pm2.65da 817 |
1
⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵 ∖ 𝐶) ∈ FinII) |