Proof of Theorem grothprim
Step | Hyp | Ref
| Expression |
1 | | axgroth4 9976 |
. 2
⊢
∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) |
2 | | 3anass 1120 |
. . . 4
⊢ ((𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ (𝑥 ∈ 𝑦 ∧ (∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))))) |
3 | | dfss2 3815 |
. . . . . . . . . . . . 13
⊢ (𝑤 ⊆ 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧)) |
4 | | elin 4025 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (𝑦 ∩ 𝑣) ↔ (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)) |
5 | 3, 4 | imbi12i 342 |
. . . . . . . . . . . 12
⊢ ((𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ (∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))) |
6 | 5 | albii 1918 |
. . . . . . . . . . 11
⊢
(∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))) |
7 | 6 | rexbii 3251 |
. . . . . . . . . 10
⊢
(∃𝑣 ∈
𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∃𝑣 ∈ 𝑦 ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))) |
8 | | df-rex 3123 |
. . . . . . . . . 10
⊢
(∃𝑣 ∈
𝑦 ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)) ↔ ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) |
9 | 7, 8 | bitri 267 |
. . . . . . . . 9
⊢
(∃𝑣 ∈
𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) |
10 | 9 | ralbii 3189 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∀𝑧 ∈ 𝑦 ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) |
11 | | df-ral 3122 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝑦 ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))))) |
12 | 10, 11 | bitri 267 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))))) |
13 | | dfss2 3815 |
. . . . . . . . . . 11
⊢ (𝑧 ⊆ 𝑦 ↔ ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) |
14 | | vex 3417 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
15 | | difexg 5035 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ V → (𝑦 ∖ 𝑧) ∈ V) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∖ 𝑧) ∈ V |
17 | | vex 3417 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
18 | | incom 4034 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∖ 𝑧) ∩ 𝑧) = (𝑧 ∩ (𝑦 ∖ 𝑧)) |
19 | | disjdif 4265 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∩ (𝑦 ∖ 𝑧)) = ∅ |
20 | 18, 19 | eqtri 2849 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∖ 𝑧) ∩ 𝑧) = ∅ |
21 | 16, 17, 20 | brdom6disj 9676 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∖ 𝑧) ≼ 𝑧 ↔ ∃𝑤(∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤)) |
22 | 21 | orbi1i 942 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦) ↔ (∃𝑤(∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)) |
23 | | 19.44v 2098 |
. . . . . . . . . . . 12
⊢
(∃𝑤((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦) ↔ (∃𝑤(∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)) |
24 | 22, 23 | bitr4i 270 |
. . . . . . . . . . 11
⊢ (((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦) ↔ ∃𝑤((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)) |
25 | 13, 24 | imbi12i 342 |
. . . . . . . . . 10
⊢ ((𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)) ↔ (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ∃𝑤((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦))) |
26 | | 19.35 1980 |
. . . . . . . . . 10
⊢
(∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)) ↔ (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ∃𝑤((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦))) |
27 | 25, 26 | bitr4i 270 |
. . . . . . . . 9
⊢ ((𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)) ↔ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦))) |
28 | | grothprimlem 9977 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑣, 𝑢} ∈ 𝑤 ↔ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢)))) |
29 | 28 | mobii 2616 |
. . . . . . . . . . . . . . . . 17
⊢
(∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ↔ ∃*𝑢∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢)))) |
30 | | df-mo 2605 |
. . . . . . . . . . . . . . . . 17
⊢
(∃*𝑢∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) ↔ ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) |
31 | 29, 30 | bitri 267 |
. . . . . . . . . . . . . . . 16
⊢
(∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ↔ ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) |
32 | 31 | ralbii 3189 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑣 ∈
𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ↔ ∀𝑣 ∈ 𝑧 ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) |
33 | | df-ral 3122 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑣 ∈
𝑧 ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡) ↔ ∀𝑣(𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡))) |
34 | 32, 33 | bitri 267 |
. . . . . . . . . . . . . 14
⊢
(∀𝑣 ∈
𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ↔ ∀𝑣(𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡))) |
35 | | df-ral 3122 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑣 ∈
(𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤 ↔ ∀𝑣(𝑣 ∈ (𝑦 ∖ 𝑧) → ∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤)) |
36 | | eldif 3808 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ (𝑦 ∖ 𝑧) ↔ (𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧)) |
37 | | grothprimlem 9977 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ({𝑢, 𝑣} ∈ 𝑤 ↔ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))) |
38 | 37 | rexbii 3251 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑢 ∈
𝑧 {𝑢, 𝑣} ∈ 𝑤 ↔ ∃𝑢 ∈ 𝑧 ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))) |
39 | | df-rex 3123 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑢 ∈
𝑧 ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))) ↔ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))) |
40 | 38, 39 | bitri 267 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑢 ∈
𝑧 {𝑢, 𝑣} ∈ 𝑤 ↔ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))) |
41 | 36, 40 | imbi12i 342 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ (𝑦 ∖ 𝑧) → ∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ ((𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧) → ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))) |
42 | | pm5.6 1029 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧) → ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))) ↔ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) |
43 | 41, 42 | bitri 267 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ (𝑦 ∖ 𝑧) → ∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) |
44 | 43 | albii 1918 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑣(𝑣 ∈ (𝑦 ∖ 𝑧) → ∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ ∀𝑣(𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) |
45 | 35, 44 | bitri 267 |
. . . . . . . . . . . . . 14
⊢
(∀𝑣 ∈
(𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤 ↔ ∀𝑣(𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) |
46 | 34, 45 | anbi12i 620 |
. . . . . . . . . . . . 13
⊢
((∀𝑣 ∈
𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ (∀𝑣(𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ ∀𝑣(𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))))) |
47 | | 19.26 1972 |
. . . . . . . . . . . . 13
⊢
(∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ↔ (∀𝑣(𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ ∀𝑣(𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))))) |
48 | 46, 47 | bitr4i 270 |
. . . . . . . . . . . 12
⊢
((∀𝑣 ∈
𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ ∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))))) |
49 | 48 | orbi1i 942 |
. . . . . . . . . . 11
⊢
(((∀𝑣 ∈
𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦) ↔ (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)) |
50 | 49 | imbi2i 328 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)) ↔ ((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))) |
51 | 50 | exbii 1947 |
. . . . . . . . 9
⊢
(∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)) ↔ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))) |
52 | 27, 51 | bitri 267 |
. . . . . . . 8
⊢ ((𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)) ↔ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))) |
53 | 52 | albii 1918 |
. . . . . . 7
⊢
(∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)) ↔ ∀𝑧∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))) |
54 | 12, 53 | anbi12i 620 |
. . . . . 6
⊢
((∀𝑧 ∈
𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ (∀𝑧(𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∀𝑧∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))) |
55 | | 19.26 1972 |
. . . . . 6
⊢
(∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))) ↔ (∀𝑧(𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∀𝑧∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))) |
56 | 54, 55 | bitr4i 270 |
. . . . 5
⊢
((∀𝑧 ∈
𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))) |
57 | 56 | anbi2i 616 |
. . . 4
⊢ ((𝑥 ∈ 𝑦 ∧ (∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)))) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))))) |
58 | 2, 57 | bitri 267 |
. . 3
⊢ ((𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))))) |
59 | 58 | exbii 1947 |
. 2
⊢
(∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))))) |
60 | 1, 59 | mpbi 222 |
1
⊢
∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))) |