Proof of Theorem grothprim
| Step | Hyp | Ref
| Expression |
| 1 | | axgroth4 10872 |
. 2
⊢
∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) |
| 2 | | 3anass 1095 |
. . . 4
⊢ ((𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ (𝑥 ∈ 𝑦 ∧ (∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))))) |
| 3 | | df-ss 3968 |
. . . . . . . . . . . . 13
⊢ (𝑤 ⊆ 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧)) |
| 4 | | elin 3967 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (𝑦 ∩ 𝑣) ↔ (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)) |
| 5 | 3, 4 | imbi12i 350 |
. . . . . . . . . . . 12
⊢ ((𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ (∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))) |
| 6 | 5 | albii 1819 |
. . . . . . . . . . 11
⊢
(∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))) |
| 7 | 6 | rexbii 3094 |
. . . . . . . . . 10
⊢
(∃𝑣 ∈
𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∃𝑣 ∈ 𝑦 ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))) |
| 8 | | df-rex 3071 |
. . . . . . . . . 10
⊢
(∃𝑣 ∈
𝑦 ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)) ↔ ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) |
| 9 | 7, 8 | bitri 275 |
. . . . . . . . 9
⊢
(∃𝑣 ∈
𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) |
| 10 | 9 | ralbii 3093 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∀𝑧 ∈ 𝑦 ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) |
| 11 | | df-ral 3062 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝑦 ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))))) |
| 12 | 10, 11 | bitri 275 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))))) |
| 13 | | df-ss 3968 |
. . . . . . . . . . 11
⊢ (𝑧 ⊆ 𝑦 ↔ ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) |
| 14 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
| 15 | 14 | difexi 5330 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∖ 𝑧) ∈ V |
| 16 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
| 17 | | disjdifr 4473 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∖ 𝑧) ∩ 𝑧) = ∅ |
| 18 | 15, 16, 17 | brdom6disj 10572 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∖ 𝑧) ≼ 𝑧 ↔ ∃𝑤(∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤)) |
| 19 | 18 | orbi1i 914 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦) ↔ (∃𝑤(∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)) |
| 20 | | 19.44v 1992 |
. . . . . . . . . . . 12
⊢
(∃𝑤((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦) ↔ (∃𝑤(∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)) |
| 21 | 19, 20 | bitr4i 278 |
. . . . . . . . . . 11
⊢ (((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦) ↔ ∃𝑤((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)) |
| 22 | 13, 21 | imbi12i 350 |
. . . . . . . . . 10
⊢ ((𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)) ↔ (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ∃𝑤((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦))) |
| 23 | | 19.35 1877 |
. . . . . . . . . 10
⊢
(∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)) ↔ (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ∃𝑤((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦))) |
| 24 | 22, 23 | bitr4i 278 |
. . . . . . . . 9
⊢ ((𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)) ↔ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦))) |
| 25 | | grothprimlem 10873 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑣, 𝑢} ∈ 𝑤 ↔ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢)))) |
| 26 | 25 | mobii 2548 |
. . . . . . . . . . . . . . . . 17
⊢
(∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ↔ ∃*𝑢∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢)))) |
| 27 | | df-mo 2540 |
. . . . . . . . . . . . . . . . 17
⊢
(∃*𝑢∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) ↔ ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) |
| 28 | 26, 27 | bitri 275 |
. . . . . . . . . . . . . . . 16
⊢
(∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ↔ ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) |
| 29 | 28 | ralbii 3093 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑣 ∈
𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ↔ ∀𝑣 ∈ 𝑧 ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) |
| 30 | | df-ral 3062 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑣 ∈
𝑧 ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡) ↔ ∀𝑣(𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡))) |
| 31 | 29, 30 | bitri 275 |
. . . . . . . . . . . . . 14
⊢
(∀𝑣 ∈
𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ↔ ∀𝑣(𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡))) |
| 32 | | df-ral 3062 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑣 ∈
(𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤 ↔ ∀𝑣(𝑣 ∈ (𝑦 ∖ 𝑧) → ∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤)) |
| 33 | | eldif 3961 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ (𝑦 ∖ 𝑧) ↔ (𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧)) |
| 34 | | grothprimlem 10873 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ({𝑢, 𝑣} ∈ 𝑤 ↔ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))) |
| 35 | 34 | rexbii 3094 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑢 ∈
𝑧 {𝑢, 𝑣} ∈ 𝑤 ↔ ∃𝑢 ∈ 𝑧 ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))) |
| 36 | | df-rex 3071 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑢 ∈
𝑧 ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))) ↔ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))) |
| 37 | 35, 36 | bitri 275 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑢 ∈
𝑧 {𝑢, 𝑣} ∈ 𝑤 ↔ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))) |
| 38 | 33, 37 | imbi12i 350 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ (𝑦 ∖ 𝑧) → ∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ ((𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧) → ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))) |
| 39 | | pm5.6 1004 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧) → ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))) ↔ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) |
| 40 | 38, 39 | bitri 275 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ (𝑦 ∖ 𝑧) → ∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) |
| 41 | 40 | albii 1819 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑣(𝑣 ∈ (𝑦 ∖ 𝑧) → ∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ ∀𝑣(𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) |
| 42 | 32, 41 | bitri 275 |
. . . . . . . . . . . . . 14
⊢
(∀𝑣 ∈
(𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤 ↔ ∀𝑣(𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) |
| 43 | 31, 42 | anbi12i 628 |
. . . . . . . . . . . . 13
⊢
((∀𝑣 ∈
𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ (∀𝑣(𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ ∀𝑣(𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))))) |
| 44 | | 19.26 1870 |
. . . . . . . . . . . . 13
⊢
(∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ↔ (∀𝑣(𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ ∀𝑣(𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))))) |
| 45 | 43, 44 | bitr4i 278 |
. . . . . . . . . . . 12
⊢
((∀𝑣 ∈
𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ ∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))))) |
| 46 | 45 | orbi1i 914 |
. . . . . . . . . . 11
⊢
(((∀𝑣 ∈
𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦) ↔ (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)) |
| 47 | 46 | imbi2i 336 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)) ↔ ((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))) |
| 48 | 47 | exbii 1848 |
. . . . . . . . 9
⊢
(∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)) ↔ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))) |
| 49 | 24, 48 | bitri 275 |
. . . . . . . 8
⊢ ((𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)) ↔ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))) |
| 50 | 49 | albii 1819 |
. . . . . . 7
⊢
(∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)) ↔ ∀𝑧∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))) |
| 51 | 12, 50 | anbi12i 628 |
. . . . . 6
⊢
((∀𝑧 ∈
𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ (∀𝑧(𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∀𝑧∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))) |
| 52 | | 19.26 1870 |
. . . . . 6
⊢
(∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))) ↔ (∀𝑧(𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∀𝑧∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))) |
| 53 | 51, 52 | bitr4i 278 |
. . . . 5
⊢
((∀𝑧 ∈
𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))) |
| 54 | 53 | anbi2i 623 |
. . . 4
⊢ ((𝑥 ∈ 𝑦 ∧ (∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)))) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))))) |
| 55 | 2, 54 | bitri 275 |
. . 3
⊢ ((𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))))) |
| 56 | 55 | exbii 1848 |
. 2
⊢
(∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))))) |
| 57 | 1, 56 | mpbi 230 |
1
⊢
∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))) |