Theorem zorn2lem6 4803

Description: Lemma for zorn2 4806.

Hypotheses

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

Assertion

Ref	Expression
zorn2lem6	⊢ (R Po A → (((w We A ⋀ x ∈ On) ⋀ ∀y ∈ x H ≠ ∅) → R Or (F “ x)))

Distinct variable groups:   x,y,w,h,t,z,f,g,u,v,A   B,h,t,f   x,F,y,z,v,u,f,g,h,t   h,G,t,f   t,C   y,D,u,v,f,t   x,R,y,z,w,g,u,v,f,t   x,H,u,v,f,t

Proof of Theorem zorn2lem6

Step	Hyp	Ref	Expression
1		zorn2lem.1	. . . . . 6 ⊢ A ∈ V
2		zorn2lem.2	. . . . . 6 ⊢ B = {f∣∃h ∈ On (f Fn h ⋀ ∀t ∈ h (f ‘t) = (G ‘(f ↾ t)))}
3		zorn2lem.3	. . . . . 6 ⊢ F = ∪B
4		zorn2lem.4	. . . . . 6 ⊢ C = {z ∈ A∣∀g ∈ ran f gRz}
5		zorn2lem.5	. . . . . 6 ⊢ D = {z ∈ A∣∀g ∈ (F “ x)gRz}
6		zorn2lem.6	. . . . . 6 ⊢ G = {⟨f, t⟩∣t = ∪{v ∈ C∣∀u ∈ C ¬ uwv}}
7		zorn2lem.7	. . . . . 6 ⊢ H = {z ∈ A∣∀g ∈ (F “ y)gRz}
8	1, 2, 3, 4, 5, 6, 7	zorn2lem5 4802	. . . . 5 ⊢ (((w We A ⋀ x ∈ On) ⋀ ∀y ∈ x H ≠ ∅) → (F “ x) ⊆ A)
9		poss 2847	. . . . 5 ⊢ ((F “ x) ⊆ A → (R Po A → R Po (F “ x)))
10	8, 9	syl 10	. . . 4 ⊢ (((w We A ⋀ x ∈ On) ⋀ ∀y ∈ x H ≠ ∅) → (R Po A → R Po (F “ x)))
11	10	com12 11	. . 3 ⊢ (R Po A → (((w We A ⋀ x ∈ On) ⋀ ∀y ∈ x H ≠ ∅) → R Po (F “ x)))
12		onelon 2978	. . . . . . . . . . . . . . . . . 18 ⊢ ((x ∈ On ⋀ b ∈ x) → b ∈ On)
13		onelon 2978	. . . . . . . . . . . . . . . . . 18 ⊢ ((x ∈ On ⋀ a ∈ x) → a ∈ On)
14	12, 13	anim12i 333	. . . . . . . . . . . . . . . . 17 ⊢ (((x ∈ On ⋀ b ∈ x) ⋀ (x ∈ On ⋀ a ∈ x)) → (b ∈ On ⋀ a ∈ On))
15	14	anandis 514	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ On ⋀ (b ∈ x ⋀ a ∈ x)) → (b ∈ On ⋀ a ∈ On))
16	15	ex 373	. . . . . . . . . . . . . . 15 ⊢ (x ∈ On → ((b ∈ x ⋀ a ∈ x) → (b ∈ On ⋀ a ∈ On)))
17		eqid 1478	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {z ∈ A∣∀g ∈ (F “ a)gRz} = {z ∈ A∣∀g ∈ (F “ a)gRz}
18	1, 2, 3, 4, 17, 6	zorn2lem2 4799	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((a ∈ On ⋀ (w We A ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅)) → (b ∈ a → (F ‘b)R(F ‘a)))
19	18	adantll 394	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((b ∈ On ⋀ a ∈ On) ⋀ (w We A ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅)) → (b ∈ a → (F ‘b)R(F ‘a)))
20		breq12 2629	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((F ‘b) = s ⋀ (F ‘a) = r) → ((F ‘b)R(F ‘a) ↔ sRr))
21	20	biimpcd 155	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((F ‘b)R(F ‘a) → (((F ‘b) = s ⋀ (F ‘a) = r) → sRr))
22	19, 21	syl6 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((b ∈ On ⋀ a ∈ On) ⋀ (w We A ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅)) → (b ∈ a → (((F ‘b) = s ⋀ (F ‘a) = r) → sRr)))
23	22	com23 32	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((b ∈ On ⋀ a ∈ On) ⋀ (w We A ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅)) → (((F ‘b) = s ⋀ (F ‘a) = r) → (b ∈ a → sRr)))
24	23	adantrrl 404	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((b ∈ On ⋀ a ∈ On) ⋀ (w We A ⋀ ({z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅ ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅))) → (((F ‘b) = s ⋀ (F ‘a) = r) → (b ∈ a → sRr)))
25	24	imp 350	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((b ∈ On ⋀ a ∈ On) ⋀ (w We A ⋀ ({z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅ ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅))) ⋀ ((F ‘b) = s ⋀ (F ‘a) = r)) → (b ∈ a → sRr))
26		eqeq12 1490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((F ‘b) = s ⋀ (F ‘a) = r) → ((F ‘b) = (F ‘a) ↔ s = r))
27		fveq2 3730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (b = a → (F ‘b) = (F ‘a))
28	26, 27	syl5bi 208	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((F ‘b) = s ⋀ (F ‘a) = r) → (b = a → s = r))
29	28	adantl 390	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((b ∈ On ⋀ a ∈ On) ⋀ (w We A ⋀ ({z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅ ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅))) ⋀ ((F ‘b) = s ⋀ (F ‘a) = r)) → (b = a → s = r))
30		eqid 1478	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {z ∈ A∣∀g ∈ (F “ b)gRz} = {z ∈ A∣∀g ∈ (F “ b)gRz}
31	1, 2, 3, 4, 30, 6	zorn2lem2 4799	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((b ∈ On ⋀ (w We A ⋀ {z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅)) → (a ∈ b → (F ‘a)R(F ‘b)))
32	31	adantlr 395	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((b ∈ On ⋀ a ∈ On) ⋀ (w We A ⋀ {z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅)) → (a ∈ b → (F ‘a)R(F ‘b)))
33		breq12 2629	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((F ‘a) = r ⋀ (F ‘b) = s) → ((F ‘a)R(F ‘b) ↔ rRs))
34	33	ancoms 438	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((F ‘b) = s ⋀ (F ‘a) = r) → ((F ‘a)R(F ‘b) ↔ rRs))
35	34	biimpcd 155	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((F ‘a)R(F ‘b) → (((F ‘b) = s ⋀ (F ‘a) = r) → rRs))
36	32, 35	syl6 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((b ∈ On ⋀ a ∈ On) ⋀ (w We A ⋀ {z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅)) → (a ∈ b → (((F ‘b) = s ⋀ (F ‘a) = r) → rRs)))
37	36	com23 32	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((b ∈ On ⋀ a ∈ On) ⋀ (w We A ⋀ {z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅)) → (((F ‘b) = s ⋀ (F ‘a) = r) → (a ∈ b → rRs)))
38	37	adantrrr 405	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((b ∈ On ⋀ a ∈ On) ⋀ (w We A ⋀ ({z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅ ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅))) → (((F ‘b) = s ⋀ (F ‘a) = r) → (a ∈ b → rRs)))
39	38	imp 350	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((b ∈ On ⋀ a ∈ On) ⋀ (w We A ⋀ ({z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅ ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅))) ⋀ ((F ‘b) = s ⋀ (F ‘a) = r)) → (a ∈ b → rRs))
40	25, 29, 39	3orim123d 903	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((b ∈ On ⋀ a ∈ On) ⋀ (w We A ⋀ ({z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅ ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅))) ⋀ ((F ‘b) = s ⋀ (F ‘a) = r)) → ((b ∈ a ⋁ b = a ⋁ a ∈ b) → (sRr ⋁ s = r ⋁ rRs)))
41		ordtri3or 2985	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Ord b ⋀ Ord a) → (b ∈ a ⋁ b = a ⋁ a ∈ b))
42		eloni 2964	. . . . . . . . . . . . . . . . . . . 20 ⊢ (b ∈ On → Ord b)
43		eloni 2964	. . . . . . . . . . . . . . . . . . . 20 ⊢ (a ∈ On → Ord a)
44	41, 42, 43	syl2an 456	. . . . . . . . . . . . . . . . . . 19 ⊢ ((b ∈ On ⋀ a ∈ On) → (b ∈ a ⋁ b = a ⋁ a ∈ b))
45	40, 44	syl5 21	. . . . . . . . . . . . . . . . . 18 ⊢ ((((b ∈ On ⋀ a ∈ On) ⋀ (w We A ⋀ ({z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅ ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅))) ⋀ ((F ‘b) = s ⋀ (F ‘a) = r)) → ((b ∈ On ⋀ a ∈ On) → (sRr ⋁ s = r ⋁ rRs)))
46	45	exp31 378	. . . . . . . . . . . . . . . . 17 ⊢ ((b ∈ On ⋀ a ∈ On) → ((w We A ⋀ ({z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅ ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅)) → (((F ‘b) = s ⋀ (F ‘a) = r) → ((b ∈ On ⋀ a ∈ On) → (sRr ⋁ s = r ⋁ rRs)))))
47	46	com4r 41	. . . . . . . . . . . . . . . 16 ⊢ ((b ∈ On ⋀ a ∈ On) → ((b ∈ On ⋀ a ∈ On) → ((w We A ⋀ ({z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅ ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅)) → (((F ‘b) = s ⋀ (F ‘a) = r) → (sRr ⋁ s = r ⋁ rRs)))))
48	47	pm2.43i 64	. . . . . . . . . . . . . . 15 ⊢ ((b ∈ On ⋀ a ∈ On) → ((w We A ⋀ ({z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅ ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅)) → (((F ‘b) = s ⋀ (F ‘a) = r) → (sRr ⋁ s = r ⋁ rRs))))
49	16, 48	syl6 22	. . . . . . . . . . . . . 14 ⊢ (x ∈ On → ((b ∈ x ⋀ a ∈ x) → ((w We A ⋀ ({z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅ ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅)) → (((F ‘b) = s ⋀ (F ‘a) = r) → (sRr ⋁ s = r ⋁ rRs)))))
50	49	exp4a 380	. . . . . . . . . . . . 13 ⊢ (x ∈ On → ((b ∈ x ⋀ a ∈ x) → (w We A → (({z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅ ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅) → (((F ‘b) = s ⋀ (F ‘a) = r) → (sRr ⋁ s = r ⋁ rRs))))))
51	50	com3r 35	. . . . . . . . . . . 12 ⊢ (w We A → (x ∈ On → ((b ∈ x ⋀ a ∈ x) → (({z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅ ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅) → (((F ‘b) = s ⋀ (F ‘a) = r) → (sRr ⋁ s = r ⋁ rRs))))))
52	51	imp 350	. . . . . . . . . . 11 ⊢ ((w We A ⋀ x ∈ On) → ((b ∈ x ⋀ a ∈ x) → (({z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅ ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅) → (((F ‘b) = s ⋀ (F ‘a) = r) → (sRr ⋁ s = r ⋁ rRs)))))
53	52	a2d 13	. . . . . . . . . 10 ⊢ ((w We A ⋀ x ∈ On) → (((b ∈ x ⋀ a ∈ x) → ({z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅ ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅)) → ((b ∈ x ⋀ a ∈ x) → (((F ‘b) = s ⋀ (F ‘a) = r) → (sRr ⋁ s = r ⋁ rRs)))))
54	7	neeq1i 1595	. . . . . . . . . . . 12 ⊢ (H ≠ ∅ ↔ {z ∈ A∣∀g ∈ (F “ y)gRz} ≠ ∅)
55	54	ralbii 1670	. . . . . . . . . . 11 ⊢ (∀y ∈ x H ≠ ∅ ↔ ∀y ∈ x {z ∈ A∣∀g ∈ (F “ y)gRz} ≠ ∅)
56		imaeq2 3408	. . . . . . . . . . . . . . . 16 ⊢ (y = b → (F “ y) = (F “ b))
57	56	raleq1d 1792	. . . . . . . . . . . . . . 15 ⊢ (y = b → (∀g ∈ (F “ y)gRz ↔ ∀g ∈ (F “ b)gRz))
58	57	rabbisdv 1810	. . . . . . . . . . . . . 14 ⊢ (y = b → {z ∈ A∣∀g ∈ (F “ y)gRz} = {z ∈ A∣∀g ∈ (F “ b)gRz})
59	58	neeq1d 1597	. . . . . . . . . . . . 13 ⊢ (y = b → ({z ∈ A∣∀g ∈ (F “ y)gRz} ≠ ∅ ↔ {z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅))
60	59	rcla4cv 1877	. . . . . . . . . . . 12 ⊢ (∀y ∈ x {z ∈ A∣∀g ∈ (F “ y)gRz} ≠ ∅ → (b ∈ x → {z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅))
61		imaeq2 3408	. . . . . . . . . . . . . . . 16 ⊢ (y = a → (F “ y) = (F “ a))
62	61	raleq1d 1792	. . . . . . . . . . . . . . 15 ⊢ (y = a → (∀g ∈ (F “ y)gRz ↔ ∀g ∈ (F “ a)gRz))
63	62	rabbisdv 1810	. . . . . . . . . . . . . 14 ⊢ (y = a → {z ∈ A∣∀g ∈ (F “ y)gRz} = {z ∈ A∣∀g ∈ (F “ a)gRz})
64	63	neeq1d 1597	. . . . . . . . . . . . 13 ⊢ (y = a → ({z ∈ A∣∀g ∈ (F “ y)gRz} ≠ ∅ ↔ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅))
65	64	rcla4cv 1877	. . . . . . . . . . . 12 ⊢ (∀y ∈ x {z ∈ A∣∀g ∈ (F “ y)gRz} ≠ ∅ → (a ∈ x → {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅))
66	60, 65	anim12d 560	. . . . . . . . . . 11 ⊢ (∀y ∈ x {z ∈ A∣∀g ∈ (F “ y)gRz} ≠ ∅ → ((b ∈ x ⋀ a ∈ x) → ({z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅ ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅)))
67	55, 66	sylbi 199	. . . . . . . . . 10 ⊢ (∀y ∈ x H ≠ ∅ → ((b ∈ x ⋀ a ∈ x) → ({z ∈ A∣∀g ∈ (F “ b)gRz} ≠ ∅ ⋀ {z ∈ A∣∀g ∈ (F “ a)gRz} ≠ ∅)))
68	53, 67	syl5 21	. . . . . . . . 9 ⊢ ((w We A ⋀ x ∈ On) → (∀y ∈ x H ≠ ∅ → ((b ∈ x ⋀ a ∈ x) → (((F ‘b) = s ⋀ (F ‘a) = r) → (sRr ⋁ s = r ⋁ rRs)))))
69	68	imp4b 365	. . . . . . . 8 ⊢ (((w We A ⋀ x ∈ On) ⋀ ∀y ∈ x H ≠ ∅) → (((b ∈ x ⋀ a ∈ x) ⋀ ((F ‘b) = s ⋀ (F ‘a) = r)) → (sRr ⋁ s = r ⋁ rRs)))
70	69	19.23advv 1299	. . . . . . 7 ⊢ (((w We A ⋀ x ∈ On) ⋀ ∀y ∈ x H ≠ ∅) → (∃b∃a((b ∈ x ⋀ a ∈ x) ⋀ ((F ‘b) = s ⋀ (F ‘a) = r)) → (sRr ⋁ s = r ⋁ rRs)))
71	2, 3	tfr1 3930	. . . . . . . . . 10 ⊢ F Fn On
72		fnfun 3591	. . . . . . . . . 10 ⊢ (F Fn On → Fun F)
73	71, 72	ax-mp 7	. . . . . . . . 9 ⊢ Fun F
74		fvelima 3770	. . . . . . . . . . . 12 ⊢ ((Fun F ⋀ s ∈ (F “ x)) → ∃b ∈ x (F ‘b) = s)
75		df-rex 1653	. . . . . . . . . . . 12 ⊢ (∃b ∈ x (F ‘b) = s ↔ ∃b(b ∈ x ⋀ (F ‘b) = s))
76	74, 75	sylib 198	. . . . . . . . . . 11 ⊢ ((Fun F ⋀ s ∈ (F “ x)) → ∃b(b ∈ x ⋀ (F ‘b) = s))
77	76	ex 373	. . . . . . . . . 10 ⊢ (Fun F → (s ∈ (F “ x) → ∃b(b ∈ x ⋀ (F ‘b) = s)))
78		fvelima 3770	. . . . . . . . . . . 12 ⊢ ((Fun F ⋀ r ∈ (F “ x)) → ∃a ∈ x (F ‘a) = r)
79		df-rex 1653	. . . . . . . . . . . 12 ⊢ (∃a ∈ x (F ‘a) = r ↔ ∃a(a ∈ x ⋀ (F ‘a) = r))
80	78, 79	sylib 198	. . . . . . . . . . 11 ⊢ ((Fun F ⋀ r ∈ (F “ x)) → ∃a(a ∈ x ⋀ (F ‘a) = r))
81	80	ex 373	. . . . . . . . . 10 ⊢ (Fun F → (r ∈ (F “ x) → ∃a(a ∈ x ⋀ (F ‘a) = r)))
82	77, 81	anim12d 560	. . . . . . . . 9 ⊢ (Fun F → ((s ∈ (F “ x) ⋀ r ∈ (F “ x)) → (∃b(b ∈ x ⋀ (F ‘b) = s) ⋀ ∃a(a ∈ x ⋀ (F ‘a) = r))))
83	73, 82	ax-mp 7	. . . . . . . 8 ⊢ ((s ∈ (F “ x) ⋀ r ∈ (F “ x)) → (∃b(b ∈ x ⋀ (F ‘b) = s) ⋀ ∃a(a ∈ x ⋀ (F ‘a) = r)))
84		an4 508	. . . . . . . . . 10 ⊢ (((b ∈ x ⋀ a ∈ x) ⋀ ((F ‘b) = s ⋀ (F ‘a) = r)) ↔ ((b ∈ x ⋀ (F ‘b) = s) ⋀ (a ∈ x ⋀ (F ‘a) = r)))
85	84	2exbii 1054	. . . . . . . . 9 ⊢ (∃b∃a((b ∈ x ⋀ a ∈ x) ⋀ ((F ‘b) = s ⋀ (F ‘a) = r)) ↔ ∃b∃a((b ∈ x ⋀ (F ‘b) = s) ⋀ (a ∈ x ⋀ (F ‘a) = r)))
86		eeanv 1325	. . . . . . . . 9 ⊢ (∃b∃a((b ∈ x ⋀ (F ‘b) = s) ⋀ (a ∈ x ⋀ (F ‘a) = r)) ↔ (∃b(b ∈ x ⋀ (F ‘b) = s) ⋀ ∃a(a ∈ x ⋀ (F ‘a) = r)))
87	85, 86	bitr 173	. . . . . . . 8 ⊢ (∃b∃a((b ∈ x ⋀ a ∈ x) ⋀ ((F ‘b) = s ⋀ (F ‘a) = r)) ↔ (∃b(b ∈ x ⋀ (F ‘b) = s) ⋀ ∃a(a ∈ x ⋀ (F ‘a) = r)))
88	83, 87	sylibr 200	. . . . . . 7 ⊢ ((s ∈ (F “ x) ⋀ r ∈ (F “ x)) → ∃b∃a((b ∈ x ⋀ a ∈ x) ⋀ ((F ‘b) = s ⋀ (F ‘a) = r)))
89	70, 88	syl5 21	. . . . . 6 ⊢ (((w We A ⋀ x ∈ On) ⋀ ∀y ∈ x H ≠ ∅) → ((s ∈ (F “ x) ⋀ r ∈ (F “ x)) → (sRr ⋁ s = r ⋁ rRs)))
90	89	19.21aivv 1289	. . . . 5 ⊢ (((w We A ⋀ x ∈ On) ⋀ ∀y ∈ x H ≠ ∅) → ∀s∀r((s ∈ (F “ x) ⋀ r ∈ (F “ x)) → (sRr ⋁ s = r ⋁ rRs)))
91		r2al 1679	. . . . 5 ⊢ (∀s ∈ (F “ x)∀r ∈ (F “ x)(sRr ⋁ s = r ⋁ rRs) ↔ ∀s∀r((s ∈ (F “ x) ⋀ r ∈ (F “ x)) → (sRr ⋁ s = r ⋁ rR