Theorem grothprim 10824

Description: The Tarski-Grothendieck Axiom ax-groth 10813 expanded into set theory primitives using 163 symbols (allowing the defined symbols ∧, ∨, ↔, and ∃). An open problem is whether a shorter equivalent exists (when expanded to primitives). (Contributed by NM, 16-Apr-2007.)

Assertion

Ref	Expression
grothprim	⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))))

Distinct variable group:   𝑥,𝑦,𝑧,𝑤,𝑣,𝑢,𝑡,ℎ,𝑔

Proof of Theorem grothprim

Step	Hyp	Ref	Expression
1		axgroth4 10822	. 2 ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)))
2		3anass 1092	. . . 4 ⊢ ((𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ (𝑥 ∈ 𝑦 ∧ (∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)))))
3		dfss2 3960	. . . . . . . . . . . . 13 ⊢ (𝑤 ⊆ 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧))
4		elin 3956	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ (𝑦 ∩ 𝑣) ↔ (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))
5	3, 4	imbi12i 350	. . . . . . . . . . . 12 ⊢ ((𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ (∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))
6	5	albii 1813	. . . . . . . . . . 11 ⊢ (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))
7	6	rexbii 3086	. . . . . . . . . 10 ⊢ (∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∃𝑣 ∈ 𝑦 ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))
8		df-rex 3063	. . . . . . . . . 10 ⊢ (∃𝑣 ∈ 𝑦 ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)) ↔ ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))))
9	7, 8	bitri 275	. . . . . . . . 9 ⊢ (∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))))
10	9	ralbii 3085	. . . . . . . 8 ⊢ (∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∀𝑧 ∈ 𝑦 ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))))
11		df-ral 3054	. . . . . . . 8 ⊢ (∀𝑧 ∈ 𝑦 ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))))
12	10, 11	bitri 275	. . . . . . 7 ⊢ (∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))))
13		dfss2 3960	. . . . . . . . . . 11 ⊢ (𝑧 ⊆ 𝑦 ↔ ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦))
14		vex 3470	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
15	14	difexi 5318	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∖ 𝑧) ∈ V
16		vex 3470	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
17		disjdifr 4464	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∖ 𝑧) ∩ 𝑧) = ∅
18	15, 16, 17	brdom6disj 10522	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∖ 𝑧) ≼ 𝑧 ↔ ∃𝑤(∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤))
19	18	orbi1i 910	. . . . . . . . . . . 12 ⊢ (((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦) ↔ (∃𝑤(∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦))
20		19.44v 1988	. . . . . . . . . . . 12 ⊢ (∃𝑤((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦) ↔ (∃𝑤(∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦))
21	19, 20	bitr4i 278	. . . . . . . . . . 11 ⊢ (((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦) ↔ ∃𝑤((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦))
22	13, 21	imbi12i 350	. . . . . . . . . 10 ⊢ ((𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)) ↔ (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ∃𝑤((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)))
23		19.35 1872	. . . . . . . . . 10 ⊢ (∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)) ↔ (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ∃𝑤((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)))
24	22, 23	bitr4i 278	. . . . . . . . 9 ⊢ ((𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)) ↔ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)))
25		grothprimlem 10823	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑣, 𝑢} ∈ 𝑤 ↔ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))))
26	25	mobii 2534	. . . . . . . . . . . . . . . . 17 ⊢ (∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ↔ ∃*𝑢∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))))
27		df-mo 2526	. . . . . . . . . . . . . . . . 17 ⊢ (∃*𝑢∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) ↔ ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡))
28	26, 27	bitri 275	. . . . . . . . . . . . . . . 16 ⊢ (∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ↔ ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡))
29	28	ralbii 3085	. . . . . . . . . . . . . . 15 ⊢ (∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ↔ ∀𝑣 ∈ 𝑧 ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡))
30		df-ral 3054	. . . . . . . . . . . . . . 15 ⊢ (∀𝑣 ∈ 𝑧 ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡) ↔ ∀𝑣(𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)))
31	29, 30	bitri 275	. . . . . . . . . . . . . 14 ⊢ (∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ↔ ∀𝑣(𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)))
32		df-ral 3054	. . . . . . . . . . . . . . 15 ⊢ (∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤 ↔ ∀𝑣(𝑣 ∈ (𝑦 ∖ 𝑧) → ∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤))
33		eldif 3950	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ (𝑦 ∖ 𝑧) ↔ (𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧))
34		grothprimlem 10823	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑢, 𝑣} ∈ 𝑤 ↔ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))
35	34	rexbii 3086	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤 ↔ ∃𝑢 ∈ 𝑧 ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))
36		df-rex 3063	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑢 ∈ 𝑧 ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))) ↔ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))
37	35, 36	bitri 275	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤 ↔ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))
38	33, 37	imbi12i 350	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 ∈ (𝑦 ∖ 𝑧) → ∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ ((𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧) → ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))
39		pm5.6 998	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧) → ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))) ↔ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))))
40	38, 39	bitri 275	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ (𝑦 ∖ 𝑧) → ∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))))
41	40	albii 1813	. . . . . . . . . . . . . . 15 ⊢ (∀𝑣(𝑣 ∈ (𝑦 ∖ 𝑧) → ∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ ∀𝑣(𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))))
42	32, 41	bitri 275	. . . . . . . . . . . . . 14 ⊢ (∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤 ↔ ∀𝑣(𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))))
43	31, 42	anbi12i 626	. . . . . . . . . . . . 13 ⊢ ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ (∀𝑣(𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ ∀𝑣(𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))))
44		19.26 1865	. . . . . . . . . . . . 13 ⊢ (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ↔ (∀𝑣(𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ ∀𝑣(𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))))
45	43, 44	bitr4i 278	. . . . . . . . . . . 12 ⊢ ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ ∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))))
46	45	orbi1i 910	. . . . . . . . . . 11 ⊢ (((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦) ↔ (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))
47	46	imbi2i 336	. . . . . . . . . 10 ⊢ (((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)) ↔ ((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))
48	47	exbii 1842	. . . . . . . . 9 ⊢ (∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)) ↔ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))
49	24, 48	bitri 275	. . . . . . . 8 ⊢ ((𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)) ↔ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))
50	49	albii 1813	. . . . . . 7 ⊢ (∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)) ↔ ∀𝑧∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))
51	12, 50	anbi12i 626	. . . . . 6 ⊢ ((∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ (∀𝑧(𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∀𝑧∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))))
52		19.26 1865	. . . . . 6 ⊢ (∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))) ↔ (∀𝑧(𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∀𝑧∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))))
53	51, 52	bitr4i 278	. . . . 5 ⊢ ((∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))))
54	53	anbi2i 622	. . . 4 ⊢ ((𝑥 ∈ 𝑦 ∧ (∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)))) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))))
55	2, 54	bitri 275	. . 3 ⊢ ((𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))))
56	55	exbii 1842	. 2 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))))
57	1, 56	mpbi 229	1 ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   ∧ w3a 1084  ∀wal 1531  ∃wex 1773   ∈ wcel 2098  ∃*wmo 2524  ∀wral 3053  ∃wrex 3062   ∖ cdif 3937   ∩ cin 3939   ⊆ wss 3940  {cpr 4622   class class class wbr 5138   ≼ cdom 8932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-reg 9582  ax-inf2 9631  ax-cc 10425  ax-ac2 10453  ax-groth 10813

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-oadd 8465  df-er 8698  df-map 8817  df-en 8935  df-dom 8936  df-sdom 8937  df-fin 8938  df-oi 9500  df-dju 9891  df-card 9929  df-acn 9932  df-ac 10106

This theorem is referenced by: (None)