Theorem grothprim 10590

Description: The Tarski-Grothendieck Axiom ax-groth 10579 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 10588	. 2 ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)))
2		3anass 1094	. . . 4 ⊢ ((𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ (𝑥 ∈ 𝑦 ∧ (∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)))))
3		dfss2 3907	. . . . . . . . . . . . 13 ⊢ (𝑤 ⊆ 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧))
4		elin 3903	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ (𝑦 ∩ 𝑣) ↔ (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))
5	3, 4	imbi12i 351	. . . . . . . . . . . 12 ⊢ ((𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ (∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))
6	5	albii 1822	. . . . . . . . . . 11 ⊢ (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))
7	6	rexbii 3181	. . . . . . . . . 10 ⊢ (∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∃𝑣 ∈ 𝑦 ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))
8		df-rex 3070	. . . . . . . . . 10 ⊢ (∃𝑣 ∈ 𝑦 ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)) ↔ ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))))
9	7, 8	bitri 274	. . . . . . . . 9 ⊢ (∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))))
10	9	ralbii 3092	. . . . . . . 8 ⊢ (∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∀𝑧 ∈ 𝑦 ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))))
11		df-ral 3069	. . . . . . . 8 ⊢ (∀𝑧 ∈ 𝑦 ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣))) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))))
12	10, 11	bitri 274	. . . . . . 7 ⊢ (∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))))
13		dfss2 3907	. . . . . . . . . . 11 ⊢ (𝑧 ⊆ 𝑦 ↔ ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦))
14		vex 3436	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
15	14	difexi 5252	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∖ 𝑧) ∈ V
16		vex 3436	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
17		disjdifr 4406	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∖ 𝑧) ∩ 𝑧) = ∅
18	15, 16, 17	brdom6disj 10288	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∖ 𝑧) ≼ 𝑧 ↔ ∃𝑤(∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤))
19	18	orbi1i 911	. . . . . . . . . . . 12 ⊢ (((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦) ↔ (∃𝑤(∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦))
20		19.44v 1996	. . . . . . . . . . . 12 ⊢ (∃𝑤((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦) ↔ (∃𝑤(∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦))
21	19, 20	bitr4i 277	. . . . . . . . . . 11 ⊢ (((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦) ↔ ∃𝑤((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦))
22	13, 21	imbi12i 351	. . . . . . . . . 10 ⊢ ((𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)) ↔ (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ∃𝑤((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)))
23		19.35 1880	. . . . . . . . . 10 ⊢ (∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)) ↔ (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ∃𝑤((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)))
24	22, 23	bitr4i 277	. . . . . . . . 9 ⊢ ((𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)) ↔ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)))
25		grothprimlem 10589	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑣, 𝑢} ∈ 𝑤 ↔ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))))
26	25	mobii 2548	. . . . . . . . . . . . . . . . 17 ⊢ (∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ↔ ∃*𝑢∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))))
27		df-mo 2540	. . . . . . . . . . . . . . . . 17 ⊢ (∃*𝑢∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) ↔ ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡))
28	26, 27	bitri 274	. . . . . . . . . . . . . . . 16 ⊢ (∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ↔ ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡))
29	28	ralbii 3092	. . . . . . . . . . . . . . 15 ⊢ (∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ↔ ∀𝑣 ∈ 𝑧 ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡))
30		df-ral 3069	. . . . . . . . . . . . . . 15 ⊢ (∀𝑣 ∈ 𝑧 ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡) ↔ ∀𝑣(𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)))
31	29, 30	bitri 274	. . . . . . . . . . . . . 14 ⊢ (∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ↔ ∀𝑣(𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)))
32		df-ral 3069	. . . . . . . . . . . . . . 15 ⊢ (∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤 ↔ ∀𝑣(𝑣 ∈ (𝑦 ∖ 𝑧) → ∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤))
33		eldif 3897	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ (𝑦 ∖ 𝑧) ↔ (𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧))
34		grothprimlem 10589	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑢, 𝑣} ∈ 𝑤 ↔ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))
35	34	rexbii 3181	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤 ↔ ∃𝑢 ∈ 𝑧 ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))
36		df-rex 3070	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑢 ∈ 𝑧 ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))) ↔ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))
37	35, 36	bitri 274	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤 ↔ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))
38	33, 37	imbi12i 351	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 ∈ (𝑦 ∖ 𝑧) → ∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ ((𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧) → ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))
39		pm5.6 999	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑣 ∈ 𝑦 ∧ ¬ 𝑣 ∈ 𝑧) → ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))) ↔ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))))
40	38, 39	bitri 274	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ (𝑦 ∖ 𝑧) → ∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))))
41	40	albii 1822	. . . . . . . . . . . . . . 15 ⊢ (∀𝑣(𝑣 ∈ (𝑦 ∖ 𝑧) → ∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ ∀𝑣(𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))))
42	32, 41	bitri 274	. . . . . . . . . . . . . 14 ⊢ (∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤 ↔ ∀𝑣(𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))))))
43	31, 42	anbi12i 627	. . . . . . . . . . . . 13 ⊢ ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ (∀𝑣(𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ ∀𝑣(𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))))
44		19.26 1873	. . . . . . . . . . . . 13 ⊢ (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ↔ (∀𝑣(𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ ∀𝑣(𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))))
45	43, 44	bitr4i 277	. . . . . . . . . . . 12 ⊢ ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ↔ ∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))))
46	45	orbi1i 911	. . . . . . . . . . 11 ⊢ (((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦) ↔ (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))
47	46	imbi2i 336	. . . . . . . . . 10 ⊢ (((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)) ↔ ((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))
48	47	exbii 1850	. . . . . . . . 9 ⊢ (∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → ((∀𝑣 ∈ 𝑧 ∃*𝑢{𝑣, 𝑢} ∈ 𝑤 ∧ ∀𝑣 ∈ (𝑦 ∖ 𝑧)∃𝑢 ∈ 𝑧 {𝑢, 𝑣} ∈ 𝑤) ∨ 𝑧 ∈ 𝑦)) ↔ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))
49	24, 48	bitri 274	. . . . . . . 8 ⊢ ((𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)) ↔ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))
50	49	albii 1822	. . . . . . 7 ⊢ (∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)) ↔ ∀𝑧∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))
51	12, 50	anbi12i 627	. . . . . 6 ⊢ ((∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ (∀𝑧(𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∀𝑧∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))))
52		19.26 1873	. . . . . 6 ⊢ (∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))) ↔ (∀𝑧(𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∀𝑧∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))))
53	51, 52	bitr4i 277	. . . . 5 ⊢ ((∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))))
54	53	anbi2i 623	. . . 4 ⊢ ((𝑥 ∈ 𝑦 ∧ (∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)))) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))))
55	2, 54	bitri 274	. . 3 ⊢ ((𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))))
56	55	exbii 1850	. 2 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))))
57	1, 56	mpbi 229	1 ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   ∧ w3a 1086  ∀wal 1537  ∃wex 1782   ∈ wcel 2106  ∃*wmo 2538  ∀wral 3064  ∃wrex 3065   ∖ cdif 3884   ∩ cin 3886   ⊆ wss 3887  {cpr 4563   class class class wbr 5074   ≼ cdom 8731

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-reg 9351  ax-inf2 9399  ax-cc 10191  ax-ac2 10219  ax-groth 10579

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-2o 8298  df-oadd 8301  df-er 8498  df-map 8617  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-oi 9269  df-dju 9659  df-card 9697  df-acn 9700  df-ac 9872

This theorem is referenced by: (None)