Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . 3
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → (𝐵 ∖ 𝐶) ∈ FinII) |
2 | | simpll1 1093 |
. . . 4
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → 𝐴 ⊆ 𝒫 𝐵) |
3 | | ssel2 3563 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → 𝑔 ∈ 𝒫 𝐵) |
4 | 3 | elpwid 4118 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → 𝑔 ⊆ 𝐵) |
5 | 4 | ssdifd 3708 |
. . . . . . . 8
⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → (𝑔 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) |
6 | | sseq1 3589 |
. . . . . . . 8
⊢ (𝑓 = (𝑔 ∖ 𝐶) → (𝑓 ⊆ (𝐵 ∖ 𝐶) ↔ (𝑔 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))) |
7 | 5, 6 | syl5ibrcom 236 |
. . . . . . 7
⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → (𝑓 = (𝑔 ∖ 𝐶) → 𝑓 ⊆ (𝐵 ∖ 𝐶))) |
8 | 7 | rexlimdva 3013 |
. . . . . 6
⊢ (𝐴 ⊆ 𝒫 𝐵 → (∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶) → 𝑓 ⊆ (𝐵 ∖ 𝐶))) |
9 | | vex 3176 |
. . . . . . 7
⊢ 𝑓 ∈ V |
10 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) |
11 | 10 | elrnmpt 5293 |
. . . . . . 7
⊢ (𝑓 ∈ V → (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶))) |
12 | 9, 11 | ax-mp 5 |
. . . . . 6
⊢ (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶)) |
13 | | selpw 4115 |
. . . . . 6
⊢ (𝑓 ∈ 𝒫 (𝐵 ∖ 𝐶) ↔ 𝑓 ⊆ (𝐵 ∖ 𝐶)) |
14 | 8, 12, 13 | 3imtr4g 284 |
. . . . 5
⊢ (𝐴 ⊆ 𝒫 𝐵 → (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → 𝑓 ∈ 𝒫 (𝐵 ∖ 𝐶))) |
15 | 14 | ssrdv 3574 |
. . . 4
⊢ (𝐴 ⊆ 𝒫 𝐵 → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ⊆ 𝒫 (𝐵 ∖ 𝐶)) |
16 | 2, 15 | syl 17 |
. . 3
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ⊆ 𝒫 (𝐵 ∖ 𝐶)) |
17 | | simplrr 797 |
. . . 4
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → 𝐶 ∈ 𝐴) |
18 | | difid 3902 |
. . . . . . 7
⊢ (𝐶 ∖ 𝐶) = ∅ |
19 | 18 | eqcomi 2619 |
. . . . . 6
⊢ ∅ =
(𝐶 ∖ 𝐶) |
20 | | difeq1 3683 |
. . . . . . . 8
⊢ (𝑔 = 𝐶 → (𝑔 ∖ 𝐶) = (𝐶 ∖ 𝐶)) |
21 | 20 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑔 = 𝐶 → (∅ = (𝑔 ∖ 𝐶) ↔ ∅ = (𝐶 ∖ 𝐶))) |
22 | 21 | rspcev 3282 |
. . . . . 6
⊢ ((𝐶 ∈ 𝐴 ∧ ∅ = (𝐶 ∖ 𝐶)) → ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶)) |
23 | 19, 22 | mpan2 703 |
. . . . 5
⊢ (𝐶 ∈ 𝐴 → ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶)) |
24 | | 0ex 4718 |
. . . . . 6
⊢ ∅
∈ V |
25 | 10 | elrnmpt 5293 |
. . . . . 6
⊢ (∅
∈ V → (∅ ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶))) |
26 | 24, 25 | ax-mp 5 |
. . . . 5
⊢ (∅
∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶)) |
27 | 23, 26 | sylibr 223 |
. . . 4
⊢ (𝐶 ∈ 𝐴 → ∅ ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
28 | | ne0i 3880 |
. . . 4
⊢ (∅
∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ≠ ∅) |
29 | 17, 27, 28 | 3syl 18 |
. . 3
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ≠ ∅) |
30 | | simpll2 1094 |
. . . 4
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) →
[⊊] Or 𝐴) |
31 | | vex 3176 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
32 | 10 | elrnmpt 5293 |
. . . . . . . 8
⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑥 = (𝑔 ∖ 𝐶))) |
33 | 31, 32 | ax-mp 5 |
. . . . . . 7
⊢ (𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑥 = (𝑔 ∖ 𝐶)) |
34 | | difeq1 3683 |
. . . . . . . . . 10
⊢ (𝑔 = 𝑒 → (𝑔 ∖ 𝐶) = (𝑒 ∖ 𝐶)) |
35 | 34 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑔 = 𝑒 → (𝑥 = (𝑔 ∖ 𝐶) ↔ 𝑥 = (𝑒 ∖ 𝐶))) |
36 | 35 | cbvrexv 3148 |
. . . . . . . 8
⊢
(∃𝑔 ∈
𝐴 𝑥 = (𝑔 ∖ 𝐶) ↔ ∃𝑒 ∈ 𝐴 𝑥 = (𝑒 ∖ 𝐶)) |
37 | | sorpssi 6841 |
. . . . . . . . . . . . . . . 16
⊢ ((
[⊊] Or 𝐴
∧ (𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → (𝑒 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑒)) |
38 | | ssdif 3707 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 ⊆ 𝑔 → (𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶)) |
39 | | ssdif 3707 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 ⊆ 𝑒 → (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶)) |
40 | 38, 39 | orim12i 537 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑒 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑒) → ((𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶) ∨ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶))) |
41 | 37, 40 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((
[⊊] Or 𝐴
∧ (𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → ((𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶) ∨ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶))) |
42 | | sseq2 3590 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ↔ (𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶))) |
43 | | sseq1 3589 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑔 ∖ 𝐶) → (𝑓 ⊆ (𝑒 ∖ 𝐶) ↔ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶))) |
44 | 42, 43 | orbi12d 742 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑔 ∖ 𝐶) → (((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)) ↔ ((𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶) ∨ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶)))) |
45 | 41, 44 | syl5ibrcom 236 |
. . . . . . . . . . . . . 14
⊢ ((
[⊊] Or 𝐴
∧ (𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → (𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))) |
46 | 45 | expr 641 |
. . . . . . . . . . . . 13
⊢ ((
[⊊] Or 𝐴
∧ 𝑒 ∈ 𝐴) → (𝑔 ∈ 𝐴 → (𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))))) |
47 | 46 | rexlimdv 3012 |
. . . . . . . . . . . 12
⊢ ((
[⊊] Or 𝐴
∧ 𝑒 ∈ 𝐴) → (∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))) |
48 | 12, 47 | syl5bi 231 |
. . . . . . . . . . 11
⊢ ((
[⊊] Or 𝐴
∧ 𝑒 ∈ 𝐴) → (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))) |
49 | 48 | ralrimiv 2948 |
. . . . . . . . . 10
⊢ ((
[⊊] Or 𝐴
∧ 𝑒 ∈ 𝐴) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))) |
50 | | sseq1 3589 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑒 ∖ 𝐶) → (𝑥 ⊆ 𝑓 ↔ (𝑒 ∖ 𝐶) ⊆ 𝑓)) |
51 | | sseq2 3590 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑒 ∖ 𝐶) → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ (𝑒 ∖ 𝐶))) |
52 | 50, 51 | orbi12d 742 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑒 ∖ 𝐶) → ((𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥) ↔ ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))) |
53 | 52 | ralbidv 2969 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑒 ∖ 𝐶) → (∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥) ↔ ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))) |
54 | 49, 53 | syl5ibrcom 236 |
. . . . . . . . 9
⊢ ((
[⊊] Or 𝐴
∧ 𝑒 ∈ 𝐴) → (𝑥 = (𝑒 ∖ 𝐶) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥))) |
55 | 54 | rexlimdva 3013 |
. . . . . . . 8
⊢ (
[⊊] Or 𝐴
→ (∃𝑒 ∈
𝐴 𝑥 = (𝑒 ∖ 𝐶) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥))) |
56 | 36, 55 | syl5bi 231 |
. . . . . . 7
⊢ (
[⊊] Or 𝐴
→ (∃𝑔 ∈
𝐴 𝑥 = (𝑔 ∖ 𝐶) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥))) |
57 | 33, 56 | syl5bi 231 |
. . . . . 6
⊢ (
[⊊] Or 𝐴
→ (𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥))) |
58 | 57 | ralrimiv 2948 |
. . . . 5
⊢ (
[⊊] Or 𝐴
→ ∀𝑥 ∈ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥)) |
59 | | sorpss 6840 |
. . . . 5
⊢ (
[⊊] Or ran (𝑔
∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∀𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥)) |
60 | 58, 59 | sylibr 223 |
. . . 4
⊢ (
[⊊] Or 𝐴
→ [⊊] Or ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
61 | 30, 60 | syl 17 |
. . 3
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) →
[⊊] Or ran (𝑔
∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
62 | | fin2i 9000 |
. . 3
⊢ ((((𝐵 ∖ 𝐶) ∈ FinII ∧ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ⊆ 𝒫 (𝐵 ∖ 𝐶)) ∧ (ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ≠ ∅ ∧ [⊊] Or
ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))) → ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
63 | 1, 16, 29, 61, 62 | syl22anc 1319 |
. 2
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
64 | | simpll3 1095 |
. . 3
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → ¬
∪ 𝐴 ∈ 𝐴) |
65 | | difeq1 3683 |
. . . . . . 7
⊢ (𝑔 = 𝑓 → (𝑔 ∖ 𝐶) = (𝑓 ∖ 𝐶)) |
66 | 65 | cbvmptv 4678 |
. . . . . 6
⊢ (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∈ 𝐴 ↦ (𝑓 ∖ 𝐶)) |
67 | 66 | elrnmpt 5293 |
. . . . 5
⊢ (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → (∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑓 ∈ 𝐴 ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) |
68 | 67 | ibi 255 |
. . . 4
⊢ (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ∃𝑓 ∈ 𝐴 ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) |
69 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ ∖ 𝐶) = (ℎ ∖ 𝐶) |
70 | | difeq1 3683 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = ℎ → (𝑔 ∖ 𝐶) = (ℎ ∖ 𝐶)) |
71 | 70 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = ℎ → ((ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶) ↔ (ℎ ∖ 𝐶) = (ℎ ∖ 𝐶))) |
72 | 71 | rspcev 3282 |
. . . . . . . . . . . . . . . 16
⊢ ((ℎ ∈ 𝐴 ∧ (ℎ ∖ 𝐶) = (ℎ ∖ 𝐶)) → ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
73 | 69, 72 | mpan2 703 |
. . . . . . . . . . . . . . 15
⊢ (ℎ ∈ 𝐴 → ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
74 | 73 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
75 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ ℎ ∈ V |
76 | | difexg 4735 |
. . . . . . . . . . . . . . 15
⊢ (ℎ ∈ V → (ℎ ∖ 𝐶) ∈ V) |
77 | 10 | elrnmpt 5293 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ ∖ 𝐶) ∈ V → ((ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶))) |
78 | 75, 76, 77 | mp2b 10 |
. . . . . . . . . . . . . 14
⊢ ((ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
79 | 74, 78 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
80 | | elssuni 4403 |
. . . . . . . . . . . . 13
⊢ ((ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → (ℎ ∖ 𝐶) ⊆ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ⊆ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
82 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) |
83 | 81, 82 | sseqtrd 3604 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶)) |
84 | 83 | adantll 746 |
. . . . . . . . . 10
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶)) |
85 | | unss2 3746 |
. . . . . . . . . . 11
⊢ ((ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶) → (𝐶 ∪ (ℎ ∖ 𝐶)) ⊆ (𝐶 ∪ (𝑓 ∖ 𝐶))) |
86 | | uncom 3719 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∪ (ℎ ∖ 𝐶)) = ((ℎ ∖ 𝐶) ∪ 𝐶) |
87 | | undif1 3995 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ ∖ 𝐶) ∪ 𝐶) = (ℎ ∪ 𝐶) |
88 | 86, 87 | eqtri 2632 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∪ (ℎ ∖ 𝐶)) = (ℎ ∪ 𝐶) |
89 | 88 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝐶 ∪ (ℎ ∖ 𝐶)) = (ℎ ∪ 𝐶)) |
90 | 64 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ¬ ∪
𝐴 ∈ 𝐴) |
91 | 17 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → 𝐶 ∈ 𝐴) |
92 | | simplrr 797 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) |
93 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 ∖ 𝐶) = (𝑥 ∖ 𝐶) |
94 | | difeq1 3683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑔 = 𝑥 → (𝑔 ∖ 𝐶) = (𝑥 ∖ 𝐶)) |
95 | 94 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑔 = 𝑥 → ((𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶) ↔ (𝑥 ∖ 𝐶) = (𝑥 ∖ 𝐶))) |
96 | 95 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ 𝐴 ∧ (𝑥 ∖ 𝐶) = (𝑥 ∖ 𝐶)) → ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
97 | 93, 96 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ 𝐴 → ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
98 | | difexg 4735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 ∈ V → (𝑥 ∖ 𝐶) ∈ V) |
99 | 10 | elrnmpt 5293 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∖ 𝐶) ∈ V → ((𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶))) |
100 | 31, 98, 99 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶)) |
101 | 97, 100 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ 𝐴 → (𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
102 | 101 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
103 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) |
104 | | ssdif0 3896 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓 ⊆ 𝐶 ↔ (𝑓 ∖ 𝐶) = ∅) |
105 | 104 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 ⊆ 𝐶 → (𝑓 ∖ 𝐶) = ∅) |
106 | 105 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → (𝑓 ∖ 𝐶) = ∅) |
107 | 103, 106 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = ∅) |
108 | | uni0c 4400 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = ∅ ↔ ∀𝑒 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))𝑒 = ∅) |
109 | 107, 108 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → ∀𝑒 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))𝑒 = ∅) |
110 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑒 = (𝑥 ∖ 𝐶) → (𝑒 = ∅ ↔ (𝑥 ∖ 𝐶) = ∅)) |
111 | 110 | rspcva 3280 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∧ ∀𝑒 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))𝑒 = ∅) → (𝑥 ∖ 𝐶) = ∅) |
112 | 102, 109,
111 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∖ 𝐶) = ∅) |
113 | | ssdif0 3896 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ⊆ 𝐶 ↔ (𝑥 ∖ 𝐶) = ∅) |
114 | 112, 113 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ 𝐶) |
115 | 114 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐶) |
116 | | unissb 4405 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∪ 𝐴
⊆ 𝐶 ↔
∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐶) |
117 | 115, 116 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∪ 𝐴 ⊆ 𝐶) |
118 | | elssuni 4403 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐶 ∈ 𝐴 → 𝐶 ⊆ ∪ 𝐴) |
119 | 118 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → 𝐶 ⊆ ∪ 𝐴) |
120 | 117, 119 | eqssd 3585 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∪ 𝐴 = 𝐶) |
121 | | simpll 786 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → 𝐶 ∈ 𝐴) |
122 | 120, 121 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∪ 𝐴 ∈ 𝐴) |
123 | 122 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) → (𝑓 ⊆ 𝐶 → ∪ 𝐴 ∈ 𝐴)) |
124 | 91, 92, 123 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝑓 ⊆ 𝐶 → ∪ 𝐴 ∈ 𝐴)) |
125 | 90, 124 | mtod 188 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ¬ 𝑓 ⊆ 𝐶) |
126 | 30 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → [⊊] Or 𝐴) |
127 | | simplrl 796 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → 𝑓 ∈ 𝐴) |
128 | | sorpssi 6841 |
. . . . . . . . . . . . . . . 16
⊢ ((
[⊊] Or 𝐴
∧ (𝑓 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓)) |
129 | 126, 127,
91, 128 | syl12anc 1316 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓)) |
130 | | orel1 396 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑓 ⊆ 𝐶 → ((𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓) → 𝐶 ⊆ 𝑓)) |
131 | 125, 129,
130 | sylc 63 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → 𝐶 ⊆ 𝑓) |
132 | | undif 4001 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ⊆ 𝑓 ↔ (𝐶 ∪ (𝑓 ∖ 𝐶)) = 𝑓) |
133 | 131, 132 | sylib 207 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝐶 ∪ (𝑓 ∖ 𝐶)) = 𝑓) |
134 | 89, 133 | sseq12d 3597 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ((𝐶 ∪ (ℎ ∖ 𝐶)) ⊆ (𝐶 ∪ (𝑓 ∖ 𝐶)) ↔ (ℎ ∪ 𝐶) ⊆ 𝑓)) |
135 | | ssun1 3738 |
. . . . . . . . . . . . 13
⊢ ℎ ⊆ (ℎ ∪ 𝐶) |
136 | | sstr 3576 |
. . . . . . . . . . . . 13
⊢ ((ℎ ⊆ (ℎ ∪ 𝐶) ∧ (ℎ ∪ 𝐶) ⊆ 𝑓) → ℎ ⊆ 𝑓) |
137 | 135, 136 | mpan 702 |
. . . . . . . . . . . 12
⊢ ((ℎ ∪ 𝐶) ⊆ 𝑓 → ℎ ⊆ 𝑓) |
138 | 134, 137 | syl6bi 242 |
. . . . . . . . . . 11
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ((𝐶 ∪ (ℎ ∖ 𝐶)) ⊆ (𝐶 ∪ (𝑓 ∖ 𝐶)) → ℎ ⊆ 𝑓)) |
139 | 85, 138 | syl5 33 |
. . . . . . . . . 10
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ((ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶) → ℎ ⊆ 𝑓)) |
140 | 84, 139 | mpd 15 |
. . . . . . . . 9
⊢
((((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ℎ ⊆ 𝑓) |
141 | 140 | ralrimiva 2949 |
. . . . . . . 8
⊢
(((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∀ℎ ∈ 𝐴 ℎ ⊆ 𝑓) |
142 | | unissb 4405 |
. . . . . . . 8
⊢ (∪ 𝐴
⊆ 𝑓 ↔
∀ℎ ∈ 𝐴 ℎ ⊆ 𝑓) |
143 | 141, 142 | sylibr 223 |
. . . . . . 7
⊢
(((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∪
𝐴 ⊆ 𝑓) |
144 | | elssuni 4403 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝐴 → 𝑓 ⊆ ∪ 𝐴) |
145 | 144 | ad2antrl 760 |
. . . . . . 7
⊢
(((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → 𝑓 ⊆ ∪ 𝐴) |
146 | 143, 145 | eqssd 3585 |
. . . . . 6
⊢
(((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∪
𝐴 = 𝑓) |
147 | | simprl 790 |
. . . . . 6
⊢
(((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → 𝑓 ∈ 𝐴) |
148 | 146, 147 | eqeltrd 2688 |
. . . . 5
⊢
(((((𝐴 ⊆
𝒫 𝐵 ∧
[⊊] Or 𝐴
∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran
(𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∪
𝐴 ∈ 𝐴) |
149 | 148 | rexlimdvaa 3014 |
. . . 4
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) →
(∃𝑓 ∈ 𝐴 ∪
ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶) → ∪ 𝐴 ∈ 𝐴)) |
150 | 68, 149 | syl5 33 |
. . 3
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ∪ 𝐴 ∈ 𝐴)) |
151 | 64, 150 | mtod 188 |
. 2
⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ FinII) → ¬
∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))) |
152 | 63, 151 | pm2.65da 598 |
1
⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or
𝐴 ∧ ¬ ∪ 𝐴
∈ 𝐴) ∧ (¬
𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵 ∖ 𝐶) ∈ FinII) |