Proof of Theorem fin23lem11
Step | Hyp | Ref
| Expression |
1 | | difeq2 4031 |
. . . . 5
⊢ (𝑐 = 𝑥 → (𝐴 ∖ 𝑐) = (𝐴 ∖ 𝑥)) |
2 | 1 | eleq1d 2822 |
. . . 4
⊢ (𝑐 = 𝑥 → ((𝐴 ∖ 𝑐) ∈ 𝐵 ↔ (𝐴 ∖ 𝑥) ∈ 𝐵)) |
3 | 2 | elrab 3602 |
. . 3
⊢ (𝑥 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵)) |
4 | | simp2r 1202 |
. . . . 5
⊢ ((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) → (𝐴 ∖ 𝑥) ∈ 𝐵) |
5 | | fin23lem11.2 |
. . . . . . . . 9
⊢ (𝑤 = (𝐴 ∖ 𝑣) → (𝜑 ↔ 𝜃)) |
6 | 5 | notbid 321 |
. . . . . . . 8
⊢ (𝑤 = (𝐴 ∖ 𝑣) → (¬ 𝜑 ↔ ¬ 𝜃)) |
7 | | simpl3 1195 |
. . . . . . . 8
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) |
8 | | difeq2 4031 |
. . . . . . . . . 10
⊢ (𝑐 = (𝐴 ∖ 𝑣) → (𝐴 ∖ 𝑐) = (𝐴 ∖ (𝐴 ∖ 𝑣))) |
9 | 8 | eleq1d 2822 |
. . . . . . . . 9
⊢ (𝑐 = (𝐴 ∖ 𝑣) → ((𝐴 ∖ 𝑐) ∈ 𝐵 ↔ (𝐴 ∖ (𝐴 ∖ 𝑣)) ∈ 𝐵)) |
10 | | difss 4046 |
. . . . . . . . . 10
⊢ (𝐴 ∖ 𝑣) ⊆ 𝐴 |
11 | | ssun1 4086 |
. . . . . . . . . . . . 13
⊢ 𝐴 ⊆ (𝐴 ∪ 𝑥) |
12 | | undif1 4390 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∖ 𝑥) ∪ 𝑥) = (𝐴 ∪ 𝑥) |
13 | 11, 12 | sseqtrri 3938 |
. . . . . . . . . . . 12
⊢ 𝐴 ⊆ ((𝐴 ∖ 𝑥) ∪ 𝑥) |
14 | | simpl2r 1229 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → (𝐴 ∖ 𝑥) ∈ 𝐵) |
15 | | simpl2l 1228 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → 𝑥 ∈ 𝒫 𝐴) |
16 | | unexg 7534 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∖ 𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝒫 𝐴) → ((𝐴 ∖ 𝑥) ∪ 𝑥) ∈ V) |
17 | 14, 15, 16 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → ((𝐴 ∖ 𝑥) ∪ 𝑥) ∈ V) |
18 | | ssexg 5216 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ((𝐴 ∖ 𝑥) ∪ 𝑥) ∧ ((𝐴 ∖ 𝑥) ∪ 𝑥) ∈ V) → 𝐴 ∈ V) |
19 | 13, 17, 18 | sylancr 590 |
. . . . . . . . . . 11
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → 𝐴 ∈ V) |
20 | | elpw2g 5237 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → ((𝐴 ∖ 𝑣) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ 𝑣) ⊆ 𝐴)) |
21 | 19, 20 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → ((𝐴 ∖ 𝑣) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ 𝑣) ⊆ 𝐴)) |
22 | 10, 21 | mpbiri 261 |
. . . . . . . . 9
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → (𝐴 ∖ 𝑣) ∈ 𝒫 𝐴) |
23 | | simpl1 1193 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → 𝐵 ⊆ 𝒫 𝐴) |
24 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ 𝐵) |
25 | 23, 24 | sseldd 3902 |
. . . . . . . . . . . 12
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ 𝒫 𝐴) |
26 | 25 | elpwid 4524 |
. . . . . . . . . . 11
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → 𝑣 ⊆ 𝐴) |
27 | | dfss4 4173 |
. . . . . . . . . . 11
⊢ (𝑣 ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ 𝑣)) = 𝑣) |
28 | 26, 27 | sylib 221 |
. . . . . . . . . 10
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → (𝐴 ∖ (𝐴 ∖ 𝑣)) = 𝑣) |
29 | 28, 24 | eqeltrd 2838 |
. . . . . . . . 9
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → (𝐴 ∖ (𝐴 ∖ 𝑣)) ∈ 𝐵) |
30 | 9, 22, 29 | elrabd 3604 |
. . . . . . . 8
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → (𝐴 ∖ 𝑣) ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵}) |
31 | 6, 7, 30 | rspcdva 3539 |
. . . . . . 7
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → ¬ 𝜃) |
32 | | simplrl 777 |
. . . . . . . . . . 11
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵)) ∧ 𝑣 ∈ 𝐵) → 𝑥 ∈ 𝒫 𝐴) |
33 | 32 | elpwid 4524 |
. . . . . . . . . 10
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵)) ∧ 𝑣 ∈ 𝐵) → 𝑥 ⊆ 𝐴) |
34 | | ssel2 3895 |
. . . . . . . . . . . 12
⊢ ((𝐵 ⊆ 𝒫 𝐴 ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ 𝒫 𝐴) |
35 | 34 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵)) ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ 𝒫 𝐴) |
36 | 35 | elpwid 4524 |
. . . . . . . . . 10
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵)) ∧ 𝑣 ∈ 𝐵) → 𝑣 ⊆ 𝐴) |
37 | | fin23lem11.3 |
. . . . . . . . . 10
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑣 ⊆ 𝐴) → (𝜒 ↔ 𝜃)) |
38 | 33, 36, 37 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵)) ∧ 𝑣 ∈ 𝐵) → (𝜒 ↔ 𝜃)) |
39 | 38 | notbid 321 |
. . . . . . . 8
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵)) ∧ 𝑣 ∈ 𝐵) → (¬ 𝜒 ↔ ¬ 𝜃)) |
40 | 39 | 3adantl3 1170 |
. . . . . . 7
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → (¬ 𝜒 ↔ ¬ 𝜃)) |
41 | 31, 40 | mpbird 260 |
. . . . . 6
⊢ (((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) ∧ 𝑣 ∈ 𝐵) → ¬ 𝜒) |
42 | 41 | ralrimiva 3105 |
. . . . 5
⊢ ((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) → ∀𝑣 ∈ 𝐵 ¬ 𝜒) |
43 | | fin23lem11.1 |
. . . . . . . 8
⊢ (𝑧 = (𝐴 ∖ 𝑥) → (𝜓 ↔ 𝜒)) |
44 | 43 | notbid 321 |
. . . . . . 7
⊢ (𝑧 = (𝐴 ∖ 𝑥) → (¬ 𝜓 ↔ ¬ 𝜒)) |
45 | 44 | ralbidv 3118 |
. . . . . 6
⊢ (𝑧 = (𝐴 ∖ 𝑥) → (∀𝑣 ∈ 𝐵 ¬ 𝜓 ↔ ∀𝑣 ∈ 𝐵 ¬ 𝜒)) |
46 | 45 | rspcev 3537 |
. . . . 5
⊢ (((𝐴 ∖ 𝑥) ∈ 𝐵 ∧ ∀𝑣 ∈ 𝐵 ¬ 𝜒) → ∃𝑧 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ¬ 𝜓) |
47 | 4, 42, 46 | syl2anc 587 |
. . . 4
⊢ ((𝐵 ⊆ 𝒫 𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) ∧ ∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑) → ∃𝑧 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ¬ 𝜓) |
48 | 47 | 3exp 1121 |
. . 3
⊢ (𝐵 ⊆ 𝒫 𝐴 → ((𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) ∈ 𝐵) → (∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑 → ∃𝑧 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ¬ 𝜓))) |
49 | 3, 48 | syl5bi 245 |
. 2
⊢ (𝐵 ⊆ 𝒫 𝐴 → (𝑥 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} → (∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑 → ∃𝑧 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ¬ 𝜓))) |
50 | 49 | rexlimdv 3202 |
1
⊢ (𝐵 ⊆ 𝒫 𝐴 → (∃𝑥 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵}∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑 → ∃𝑧 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ¬ 𝜓)) |