Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem zornlem7 3609

Description: Lemma for Zorn's lemma.

**Hypotheses**
Ref	Expression
zornlem.1	⊢ A ∈ V
zornlem.2	⊢ B = {f∣∃h ∈ On (f Fn h ∧ ∀t ∈ h (f ‘t) = (G ‘(f ↾ t)))}
zornlem.3	⊢ F = ∪B
zornlem.4	⊢ C = {z ∈ A∣∀g ∈ ran fgRz}
zornlem.5	⊢ D = {z ∈ A∣∀g ∈ (F “ x)gRz}
zornlem.6	⊢ G = {⟨f, t⟩∣t = ∪{v ∈ C∣∀u ∈ C ¬ uwv}}
zornlem.7	⊢ H = {z ∈ A∣∀g ∈ (F “ y)gRz}

**Assertion**
Ref	Expression
zornlem7	⊢ ((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) → ∃a ∈ A ∀b ∈ A ¬ aRb)

Distinct variable group(s): x,y,w,h,t,z,f,g,u,v,r,s,a,b,A B,h,t,f x,F,y,z,v,u,f,g,h,t,r,s,a,b h,G,t,f t,C y,D,u,v,f,t,a,b x,R,y,z,w,g,u,v,f,t,s,r,a,b x,H,u,v,f,t,s,r,a,b

**Proof of Theorem zornlem7**
Step	Hyp	Ref	Expression
1		zornlem.1	. . 3 ⊢ A ∈ V
2	1	weth 3602	. 2 ⊢ ∃w w We A
3		zornlem.2	. . . . . . . 8 ⊢ B = {f∣∃h ∈ On (f Fn h ∧ ∀t ∈ h (f ‘t) = (G ‘(f ↾ t)))}
4		zornlem.3	. . . . . . . 8 ⊢ F = ∪B
5		zornlem.4	. . . . . . . 8 ⊢ C = {z ∈ A∣∀g ∈ ran fgRz}
6		zornlem.5	. . . . . . . 8 ⊢ D = {z ∈ A∣∀g ∈ (F “ x)gRz}
7		zornlem.6	. . . . . . . 8 ⊢ G = {⟨f, t⟩∣t = ∪{v ∈ C∣∀u ∈ C ¬ uwv}}
8	1, 3, 4, 5, 6, 7	zornlem4 3606	. . . . . . 7 ⊢ ((R Po A ∧ w We A) → ∃x ∈ On D = ∅)
9		imaeq2 2603	. . . . . . . . . . . 12 ⊢ (x = y → (F “ x) = (F “ y))
10		raleq 1324	. . . . . . . . . . . 12 ⊢ ((F “ x) = (F “ y) → (∀g ∈ (F “ x)gRz ↔ ∀g ∈ (F “ y)gRz))
11	9, 10	syl 12	. . . . . . . . . . 11 ⊢ (x = y → (∀g ∈ (F “ x)gRz ↔ ∀g ∈ (F “ y)gRz))
12	11	birabsdv 1344	. . . . . . . . . 10 ⊢ (x = y → {z ∈ A∣∀g ∈ (F “ x)gRz} = {z ∈ A∣∀g ∈ (F “ y)gRz})
13		zornlem.7	. . . . . . . . . 10 ⊢ H = {z ∈ A∣∀g ∈ (F “ y)gRz}
14	12, 6, 13	3eqtr4g 1147	. . . . . . . . 9 ⊢ (x = y → D = H)
15	14	cleq1d 1109	. . . . . . . 8 ⊢ (x = y → (D = ∅ ↔ H = ∅))
16	15	onminex 2275	. . . . . . 7 ⊢ (∃x ∈ On D = ∅ → ∃x ∈ On (D = ∅ ∧ ∀y ∈ x ¬ H = ∅))
17	1, 3, 4, 5, 6, 7, 13	zornlem5 3607	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → (F “ x) ⊆ A)
18	17	a1i 7	. . . . . . . . . . . . . . . . . . 19 ⊢ (R Po A → (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → (F “ x) ⊆ A))
19	1, 3, 4, 5, 6, 7, 13	zornlem6 3608	. . . . . . . . . . . . . . . . . . 19 ⊢ (R Po A → (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → R Or (F “ x)))
20	18, 19	jcad 455	. . . . . . . . . . . . . . . . . 18 ⊢ (R Po A → (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → ((F “ x) ⊆ A ∧ R Or (F “ x))))
21	3, 4	tfrlem7 2955	. . . . . . . . . . . . . . . . . . . 20 ⊢ Fun F
22		visset 1350	. . . . . . . . . . . . . . . . . . . . 21 ⊢ x ∈ V
23	22	funimaex 2716	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Fun F → (F “ x) ∈ V)
24	21, 23	ax-mp 6	. . . . . . . . . . . . . . . . . . 19 ⊢ (F “ x) ∈ V
25		sseq1 1521	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (s = (F “ x) → (s ⊆ A ↔ (F “ x) ⊆ A))
26		soeq2 2142	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (s = (F “ x) → (R Or s ↔ R Or (F “ x)))
27	25, 26	anbi12d 476	. . . . . . . . . . . . . . . . . . . 20 ⊢ (s = (F “ x) → ((s ⊆ A ∧ R Or s) ↔ ((F “ x) ⊆ A ∧ R Or (F “ x))))
28		raleq 1324	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (s = (F “ x) → (∀r ∈ s (rRa ∨ r = a) ↔ ∀r ∈ (F “ x)(rRa ∨ r = a)))
29	28	birexdv 1220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (s = (F “ x) → (∃a ∈ A ∀r ∈ s (rRa ∨ r = a) ↔ ∃a ∈ A ∀r ∈ (F “ x)(rRa ∨ r = a)))
30	27, 29	imbi12d 474	. . . . . . . . . . . . . . . . . . 19 ⊢ (s = (F “ x) → (((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a)) ↔ (((F “ x) ⊆ A ∧ R Or (F “ x)) → ∃a ∈ A ∀r ∈ (F “ x)(rRa ∨ r = a))))
31	24, 30	cla4v 1400	. . . . . . . . . . . . . . . . . 18 ⊢ (∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a)) → (((F “ x) ⊆ A ∧ R Or (F “ x)) → ∃a ∈ A ∀r ∈ (F “ x)(rRa ∨ r = a)))
32	20, 31	sylan9 359	. . . . . . . . . . . . . . . . 17 ⊢ ((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) → (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → ∃a ∈ A ∀r ∈ (F “ x)(rRa ∨ r = a)))
33	32	adantld 307	. . . . . . . . . . . . . . . 16 ⊢ ((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) → ((D = ∅ ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅)) → ∃a ∈ A ∀r ∈ (F “ x)(rRa ∨ r = a)))
34	33	imp 277	. . . . . . . . . . . . . . 15 ⊢ (((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) ∧ (D = ∅ ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅))) → ∃a ∈ A ∀r ∈ (F “ x)(rRa ∨ r = a))
35		noel 1711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ¬ b ∈ ∅
36	17	sseld 1506	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → (r ∈ (F “ x) → r ∈ A))
37		potr 2134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((R Po A ∧ (r ∈ A ∧ a ∈ A ∧ b ∈ A)) → ((rRa ∧ aRb) → rRb))
38		3anass 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((r ∈ A ∧ a ∈ A ∧ b ∈ A) ↔ (r ∈ A ∧ (a ∈ A ∧ b ∈ A)))
39	37, 38	sylan2br 348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((R Po A ∧ (r ∈ A ∧ (a ∈ A ∧ b ∈ A))) → ((rRa ∧ aRb) → rRb))
40	39	exp3a 292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((R Po A ∧ (r ∈ A ∧ (a ∈ A ∧ b ∈ A))) → (rRa → (aRb → rRb)))
41	40	com23 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((R Po A ∧ (r ∈ A ∧ (a ∈ A ∧ b ∈ A))) → (aRb → (rRa → rRb)))
42	41	imp 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((R Po A ∧ (r ∈ A ∧ (a ∈ A ∧ b ∈ A))) ∧ aRb) → (rRa → rRb))
43		breq1 2065	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (r = a → (rRb ↔ aRb))
44	43	biimprcd 138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (aRb → (r = a → rRb))
45	44	adantl 305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((R Po A ∧ (r ∈ A ∧ (a ∈ A ∧ b ∈ A))) ∧ aRb) → (r = a → rRb))
46	42, 45	jaod 329	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((R Po A ∧ (r ∈ A ∧ (a ∈ A ∧ b ∈ A))) ∧ aRb) → ((rRa ∨ r = a) → rRb))
47	46	exp42 300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (R Po A → (r ∈ A → ((a ∈ A ∧ b ∈ A) → (aRb → ((rRa ∨ r = a) → rRb)))))
48	36, 47	sylan9r 360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅)) → (r ∈ (F “ x) → ((a ∈ A ∧ b ∈ A) → (aRb → ((rRa ∨ r = a) → rRb)))))
49	48	com24 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅)) → (aRb → ((a ∈ A ∧ b ∈ A) → (r ∈ (F “ x) → ((rRa ∨ r = a) → rRb)))))
50	49	com23 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅)) → ((a ∈ A ∧ b ∈ A) → (aRb → (r ∈ (F “ x) → ((rRa ∨ r = a) → rRb)))))
51	50	imp31 280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅)) ∧ (a ∈ A ∧ b ∈ A)) ∧ aRb) → (r ∈ (F “ x) → ((rRa ∨ r = a) → rRb)))
52	51	a2d 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((((R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅)) ∧ (a ∈ A ∧ b ∈ A)) ∧ aRb) → ((r ∈ (F “ x) → (rRa ∨ r = a)) → (r ∈ (F “ x) → rRb)))
53	52	19.20dv 946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((((R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅)) ∧ (a ∈ A ∧ b ∈ A)) ∧ aRb) → (∀r(r ∈ (F “ x) → (rRa ∨ r = a)) → ∀r(r ∈ (F “ x) → rRb)))
54		df-ral 1205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (∀r ∈ (F “ x)(rRa ∨ r = a) ↔ ∀r(r ∈ (F “ x) → (rRa ∨ r = a)))
55		df-ral 1205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (∀r ∈ (F “ x)rRb ↔ ∀r(r ∈ (F “ x) → rRb))
56	53, 54, 55	3imtr4g 426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅)) ∧ (a ∈ A ∧ b ∈ A)) ∧ aRb) → (∀r ∈ (F “ x)(rRa ∨ r = a) → ∀r ∈ (F “ x)rRb))
57	6	cleq1i 1108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (D = ∅ ↔ {z ∈ A∣∀g ∈ (F “ x)gRz} = ∅)
58		eleq2 1150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ({z ∈ A∣∀g ∈ (F “ x)gRz} = ∅ → (b ∈ {z ∈ A∣∀g ∈ (F “ x)gRz} ↔ b ∈ ∅))
59	57, 58	sylbi 174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (D = ∅ → (b ∈ {z ∈ A∣∀g ∈ (F “ x)gRz} ↔ b ∈ ∅))
60		breq2 2066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (z = b → (gRz ↔ gRb))
61	60	biraldv 1219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (z = b → (∀g ∈ (F “ x)gRz ↔ ∀g ∈ (F “ x)gRb))
62	61	elrab 1422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (b ∈ {z ∈ A∣∀g ∈ (F “ x)gRz} ↔ (b ∈ A ∧ ∀g ∈ (F “ x)gRb))
63	59, 62	syl5bbr 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (D = ∅ → ((b ∈ A ∧ ∀g ∈ (F “ x)gRb) ↔ b ∈ ∅))
64	63	biimpd 135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (D = ∅ → ((b ∈ A ∧ ∀g ∈ (F “ x)gRb) → b ∈ ∅))
65	64	exp3a 292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (D = ∅ → (b ∈ A → (∀g ∈ (F “ x)gRb → b ∈ ∅)))
66	65	imp 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((D = ∅ ∧ b ∈ A) → (∀g ∈ (F “ x)gRb → b ∈ ∅))
67		breq1 2065	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (r = g → (rRb ↔ gRb))
68	67	cbvralv 1333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (∀r ∈ (F “ x)rRb ↔ ∀g ∈ (F “ x)gRb)
69	66, 68	syl5ib 181	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((D = ∅ ∧ b ∈ A) → (∀r ∈ (F “ x)rRb → b ∈ ∅))
70	56, 69	sylan9r 360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((D = ∅ ∧ b ∈ A) ∧ (((R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅)) ∧ (a ∈ A ∧ b ∈ A)) ∧ aRb)) → (∀r ∈ (F “ x)(rRa ∨ r = a) → b ∈ ∅))
71	70	exp32 294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((D = ∅ ∧ b ∈ A) → (((R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅)) ∧ (a ∈ A ∧ b ∈ A)) → (aRb → (∀r ∈ (F “ x)(rRa ∨ r = a) → b ∈ ∅))))
72	71	com34 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((D = ∅ ∧ b ∈ A) → (((R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅)) ∧ (a ∈ A ∧ b ∈ A)) → (∀r ∈ (F “ x)(rRa ∨ r = a) → (aRb → b ∈ ∅))))
73	72	imp31 280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((D = ∅ ∧ b ∈ A) ∧ ((R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅)) ∧ (a ∈ A ∧ b ∈ A))) ∧ ∀r ∈ (F “ x)(rRa ∨ r = a)) → (aRb → b ∈ ∅))
74	35, 73	mtoi 94	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((D = ∅ ∧ b ∈ A) ∧ ((R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅)) ∧ (a ∈ A ∧ b ∈ A))) ∧ ∀r ∈ (F “ x)(rRa ∨ r = a)) → ¬ aRb)
75	74	exp42 300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((D = ∅ ∧ b ∈ A) → ((R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅)) → ((a ∈ A ∧ b ∈ A) → (∀r ∈ (F “ x)(rRa ∨ r = a) → ¬ aRb))))
76	75	exp4a 295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((D = ∅ ∧ b ∈ A) → ((R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅)) → (a ∈ A → (b ∈ A → (∀r ∈ (F “ x)(rRa ∨ r = a) → ¬ aRb)))))
77	76	com34 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((D = ∅ ∧ b ∈ A) → ((R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅)) → (b ∈ A → (a ∈ A → (∀r ∈ (F “ x)(rRa ∨ r = a) → ¬ aRb)))))
78	77	exp 291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (D = ∅ → (b ∈ A → ((R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅)) → (b ∈ A → (a ∈ A → (∀r ∈ (F “ x)(rRa ∨ r = a) → ¬ aRb))))))
79	78	com4r 41	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (b ∈ A → (D = ∅ → (b ∈ A → ((R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅)) → (a ∈ A → (∀r ∈ (F “ x)(rRa ∨ r = a) → ¬ aRb))))))
80	79	pm2.43a 60	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (b ∈ A → (D = ∅ → ((R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅)) → (a ∈ A → (∀r ∈ (F “ x)(rRa ∨ r = a) → ¬ aRb)))))
81	80	imp3a 279	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (b ∈ A → ((D = ∅ ∧ (R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅))) → (a ∈ A → (∀r ∈ (F “ x)(rRa ∨ r = a) → ¬ aRb))))
82	81	com4l 39	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((D = ∅ ∧ (R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅))) → (a ∈ A → (∀r ∈ (F “ x)(rRa ∨ r = a) → (b ∈ A → ¬ aRb))))
83	82	imp3a 279	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((D = ∅ ∧ (R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅))) → ((a ∈ A ∧ ∀r ∈ (F “ x)(rRa ∨ r = a)) → (b ∈ A → ¬ aRb)))
84	83	19.21adv 945	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((D = ∅ ∧ (R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅))) → ((a ∈ A ∧ ∀r ∈ (F “ x)(rRa ∨ r = a)) → ∀b(b ∈ A → ¬ aRb)))
85		df-ral 1205	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀b ∈ A ¬ aRb ↔ ∀b(b ∈ A → ¬ aRb))
86	84, 85	syl6ibr 186	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((D = ∅ ∧ (R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅))) → ((a ∈ A ∧ ∀r ∈ (F “ x)(rRa ∨ r = a)) → ∀b ∈ A ¬ aRb))
87	86	exp3a 292	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((D = ∅ ∧ (R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅))) → (a ∈ A → (∀r ∈ (F “ x)(rRa ∨ r = a) → ∀b ∈ A ¬ aRb)))
88	87	imdistand 342	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((D = ∅ ∧ (R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅))) → ((a ∈ A ∧ ∀r ∈ (F “ x)(rRa ∨ r = a)) → (a ∈ A ∧ ∀b ∈ A ¬ aRb)))
89	88	19.22dv 947	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((D = ∅ ∧ (R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅))) → (∃a(a ∈ A ∧ ∀r ∈ (F “ x)(rRa ∨ r = a)) → ∃a(a ∈ A ∧ ∀b ∈ A ¬ aRb)))
90		df-rex 1206	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃a ∈ A ∀r ∈ (F “ x)(rRa ∨ r = a) ↔ ∃a(a ∈ A ∧ ∀r ∈ (F “ x)(rRa ∨ r = a)))
91		df-rex 1206	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃a ∈ A ∀b ∈ A ¬ aRb ↔ ∃a(a ∈ A ∧ ∀b ∈ A ¬ aRb))
92	89, 90, 91	3imtr4g 426	. . . . . . . . . . . . . . . . . . 19 ⊢ ((D = ∅ ∧ (R Po A ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅))) → (∃a ∈ A ∀r ∈ (F “ x)(rRa ∨ r = a) → ∃a ∈ A ∀b ∈ A ¬ aRb))
93	92	exp32 294	. . . . . . . . . . . . . . . . . 18 ⊢ (D = ∅ → (R Po A → (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → (∃a ∈ A ∀r ∈ (F “ x)(rRa ∨ r = a) → ∃a ∈ A ∀b ∈ A ¬ aRb))))
94	93	com12 13	. . . . . . . . . . . . . . . . 17 ⊢ (R Po A → (D = ∅ → (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → (∃a ∈ A ∀r ∈ (F “ x)(rRa ∨ r = a) → ∃a ∈ A ∀b ∈ A ¬ aRb))))
95	94	adantr 306	. . . . . . . . . . . . . . . 16 ⊢ ((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) → (D = ∅ → (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → (∃a ∈ A ∀r ∈ (F “ x)(rRa ∨ r = a) → ∃a ∈ A ∀b ∈ A ¬ aRb))))
96	95	imp32 281	. . . . . . . . . . . . . . 15 ⊢ (((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) ∧ (D = ∅ ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅))) → (∃a ∈ A ∀r ∈ (F “ x)(rRa ∨ r = a) → ∃a ∈ A ∀b ∈ A ¬ aRb))
97	34, 96	mpd 46	. . . . . . . . . . . . . 14 ⊢ (((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) ∧ (D = ∅ ∧ ((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅))) → ∃a ∈ A ∀b ∈ A ¬ aRb)
98	97	exp45 303	. . . . . . . . . . . . 13 ⊢ ((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) → (D = ∅ → ((w We A ∧ x ∈ On) → (∀y ∈ x ¬ H = ∅ → ∃a ∈ A ∀b ∈ A ¬ aRb))))
99	98	com23 32	. . . . . . . . . . . 12 ⊢ ((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) → ((w We A ∧ x ∈ On) → (D = ∅ → (∀y ∈ x ¬ H = ∅ → ∃a ∈ A ∀b ∈ A ¬ aRb))))
100	99	exp3a 292	. . . . . . . . . . 11 ⊢ ((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) → (w We A → (x ∈ On → (D = ∅ → (∀y ∈ x ¬ H = ∅ → ∃a ∈ A ∀b ∈ A ¬ aRb)))))
101	100	imp 277	. . . . . . . . . 10 ⊢ (((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) ∧ w We A) → (x ∈ On → (D = ∅ → (∀y ∈ x ¬ H = ∅ → ∃a ∈ A ∀b ∈ A ¬ aRb))))
102	101	imp4a 282	. . . . . . . . 9 ⊢ (((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) ∧ w We A) → (x ∈ On → ((D = ∅ ∧ ∀y ∈ x ¬ H = ∅) → ∃a ∈ A ∀b ∈ A ¬ aRb)))
103	102	com3l 34	. . . . . . . 8 ⊢ (x ∈ On → ((D = ∅ ∧ ∀y ∈ x ¬ H = ∅) → (((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) ∧ w We A) → ∃a ∈ A ∀b ∈ A ¬ aRb)))
104	103	r19.23aiv 1284	. . . . . . 7 ⊢ (∃x ∈ On (D = ∅ ∧ ∀y ∈ x ¬ H = ∅) → (((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) ∧ w We A) → ∃a ∈ A ∀b ∈ A ¬ aRb))
105	8, 16, 104	3syl 21	. . . . . 6 ⊢ ((R Po A ∧ w We A) → (((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) ∧ w We A) → ∃a ∈ A ∀b ∈ A ¬ aRb))
106	105	adantlr 310	. . . . 5 ⊢ (((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) ∧ w We A) → (((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) ∧ w We A) → ∃a ∈ A ∀b ∈ A ¬ aRb))
107	106	pm2.43i 58	. . . 4 ⊢ (((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) ∧ w We A) → ∃a ∈ A ∀b ∈ A ¬ aRb)
108	107	exp 291	. . 3 ⊢ ((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) → (w We A → ∃a ∈ A ∀b ∈ A ¬ aRb))
109	108	19.23adv 954	. 2 ⊢ ((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) → (∃w w We A → ∃a ∈ A ∀b ∈ A ¬ aRb))
110	2, 109	mpi 44	1 ⊢ ((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) → ∃a ∈ A ∀b ∈ A ¬ aRb)

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∨ wo 195 ∧ wa 196 ∧ w3a 581 ∀wal 672 ∃wex 678 = weq 797 {cab 1090 = wceq 1091 ∈ wcel 1092 ∀wral 1201 ∃wrex 1202 {crab 1204 Vcvv 1348 ⊆ wss 1487 ∅c0 1707 ∪cuni 1919 class class class wbr 2054 {copab 2055 Po wpo 2058 Or wor 2059</