Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem zornlem6 3608

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
zornlem6	⊢ (R Po A → (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → R Or (F “ x)))

Distinct variable group(s): 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 zornlem6**
Step	Hyp	Ref	Expression
1		zornlem.1	. . . . . 6 ⊢ A ∈ V
2		zornlem.2	. . . . . 6 ⊢ B = {f∣∃h ∈ On (f Fn h ∧ ∀t ∈ h (f ‘t) = (G ‘(f ↾ t)))}
3		zornlem.3	. . . . . 6 ⊢ F = ∪B
4		zornlem.4	. . . . . 6 ⊢ C = {z ∈ A∣∀g ∈ ran fgRz}
5		zornlem.5	. . . . . 6 ⊢ D = {z ∈ A∣∀g ∈ (F “ x)gRz}
6		zornlem.6	. . . . . 6 ⊢ G = {⟨f, t⟩∣t = ∪{v ∈ C∣∀u ∈ C ¬ uwv}}
7		zornlem.7	. . . . . 6 ⊢ H = {z ∈ A∣∀g ∈ (F “ y)gRz}
8	1, 2, 3, 4, 5, 6, 7	zornlem5 3607	. . . . 5 ⊢ (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → (F “ x) ⊆ A)
9		poss 2129	. . . . 5 ⊢ ((F “ x) ⊆ A → (R Po A → R Po (F “ x)))
10	8, 9	syl 12	. . . 4 ⊢ (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → (R Po A → R Po (F “ x)))
11	10	com12 13	. . 3 ⊢ (R Po A → (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → R Po (F “ x)))
12		onelon 2223	. . . . . . . . . . . . . . . . . 18 ⊢ ((x ∈ On ∧ a ∈ x) → a ∈ On)
13		onelon 2223	. . . . . . . . . . . . . . . . . 18 ⊢ ((x ∈ On ∧ b ∈ x) → b ∈ On)
14	12, 13	anim12i 268	. . . . . . . . . . . . . . . . 17 ⊢ (((x ∈ On ∧ a ∈ x) ∧ (x ∈ On ∧ b ∈ x)) → (a ∈ On ∧ b ∈ On))
15	14	anandis 394	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ On ∧ (a ∈ x ∧ b ∈ x)) → (a ∈ On ∧ b ∈ On))
16	15	exp 291	. . . . . . . . . . . . . . 15 ⊢ (x ∈ On → ((a ∈ x ∧ b ∈ x) → (a ∈ On ∧ b ∈ On)))
17		cleqid 1102	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {z ∈ A∣∀g ∈ (F “ b)gRz} = {z ∈ A∣∀g ∈ (F “ b)gRz}
18	1, 2, 3, 4, 17, 6	zornlem2 3604	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((b ∈ On ∧ (w We A ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅)) → (a ∈ b → (F ‘a)R(F ‘b)))
19	18	adantll 309	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((a ∈ On ∧ b ∈ On) ∧ (w We A ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅)) → (a ∈ b → (F ‘a)R(F ‘b)))
20		breq12 2067	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((F ‘a) = r ∧ (F ‘b) = s) → ((F ‘a)R(F ‘b) ↔ rRs))
21	20	biimpcd 137	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((F ‘a)R(F ‘b) → (((F ‘a) = r ∧ (F ‘b) = s) → rRs))
22	19, 21	syl6 23	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((a ∈ On ∧ b ∈ On) ∧ (w We A ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅)) → (a ∈ b → (((F ‘a) = r ∧ (F ‘b) = s) → rRs)))
23	22	com23 32	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((a ∈ On ∧ b ∈ On) ∧ (w We A ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅)) → (((F ‘a) = r ∧ (F ‘b) = s) → (a ∈ b → rRs)))
24	23	adantrrl 318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((a ∈ On ∧ b ∈ On) ∧ (w We A ∧ (¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅ ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅))) → (((F ‘a) = r ∧ (F ‘b) = s) → (a ∈ b → rRs)))
25	24	imp 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((a ∈ On ∧ b ∈ On) ∧ (w We A ∧ (¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅ ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅))) ∧ ((F ‘a) = r ∧ (F ‘b) = s)) → (a ∈ b → rRs))
26		cleq12 1113	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((F ‘a) = r ∧ (F ‘b) = s) → ((F ‘a) = (F ‘b) ↔ r = s))
27		fveq2 2832	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (a = b → (F ‘a) = (F ‘b))
28	26, 27	syl5bi 183	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((F ‘a) = r ∧ (F ‘b) = s) → (a = b → r = s))
29	28	adantl 305	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((a ∈ On ∧ b ∈ On) ∧ (w We A ∧ (¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅ ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅))) ∧ ((F ‘a) = r ∧ (F ‘b) = s)) → (a = b → r = s))
30		cleqid 1102	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {z ∈ A∣∀g ∈ (F “ a)gRz} = {z ∈ A∣∀g ∈ (F “ a)gRz}
31	1, 2, 3, 4, 30, 6	zornlem2 3604	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((a ∈ On ∧ (w We A ∧ ¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅)) → (b ∈ a → (F ‘b)R(F ‘a)))
32	31	adantlr 310	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((a ∈ On ∧ b ∈ On) ∧ (w We A ∧ ¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅)) → (b ∈ a → (F ‘b)R(F ‘a)))
33		breq12 2067	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((F ‘b) = s ∧ (F ‘a) = r) → ((F ‘b)R(F ‘a) ↔ sRr))
34	33	ancoms 334	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((F ‘a) = r ∧ (F ‘b) = s) → ((F ‘b)R(F ‘a) ↔ sRr))
35	34	biimpcd 137	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((F ‘b)R(F ‘a) → (((F ‘a) = r ∧ (F ‘b) = s) → sRr))
36	32, 35	syl6 23	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((a ∈ On ∧ b ∈ On) ∧ (w We A ∧ ¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅)) → (b ∈ a → (((F ‘a) = r ∧ (F ‘b) = s) → sRr)))
37	36	com23 32	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((a ∈ On ∧ b ∈ On) ∧ (w We A ∧ ¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅)) → (((F ‘a) = r ∧ (F ‘b) = s) → (b ∈ a → sRr)))
38	37	adantrrr 319	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((a ∈ On ∧ b ∈ On) ∧ (w We A ∧ (¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅ ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅))) → (((F ‘a) = r ∧ (F ‘b) = s) → (b ∈ a → sRr)))
39	38	imp 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((a ∈ On ∧ b ∈ On) ∧ (w We A ∧ (¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅ ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅))) ∧ ((F ‘a) = r ∧ (F ‘b) = s)) → (b ∈ a → sRr))
40	25, 29, 39	im3ord 637	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((a ∈ On ∧ b ∈ On) ∧ (w We A ∧ (¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅ ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅))) ∧ ((F ‘a) = r ∧ (F ‘b) = s)) → ((a ∈ b ∨ a = b ∨ b ∈ a) → (rRs ∨ r = s ∨ sRr)))
41		ordtri3or 2230	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Ord a ∧ Ord b) → (a ∈ b ∨ a = b ∨ b ∈ a))
42		eloni 2209	. . . . . . . . . . . . . . . . . . . 20 ⊢ (a ∈ On → Ord a)
43		eloni 2209	. . . . . . . . . . . . . . . . . . . 20 ⊢ (b ∈ On → Ord b)
44	41, 42, 43	syl2an 349	. . . . . . . . . . . . . . . . . . 19 ⊢ ((a ∈ On ∧ b ∈ On) → (a ∈ b ∨ a = b ∨ b ∈ a))
45	40, 44	syl5 22	. . . . . . . . . . . . . . . . . 18 ⊢ ((((a ∈ On ∧ b ∈ On) ∧ (w We A ∧ (¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅ ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅))) ∧ ((F ‘a) = r ∧ (F ‘b) = s)) → ((a ∈ On ∧ b ∈ On) → (rRs ∨ r = s ∨ sRr)))
46	45	exp31 293	. . . . . . . . . . . . . . . . 17 ⊢ ((a ∈ On ∧ b ∈ On) → ((w We A ∧ (¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅ ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅)) → (((F ‘a) = r ∧ (F ‘b) = s) → ((a ∈ On ∧ b ∈ On) → (rRs ∨ r = s ∨ sRr)))))
47	46	com4r 41	. . . . . . . . . . . . . . . 16 ⊢ ((a ∈ On ∧ b ∈ On) → ((a ∈ On ∧ b ∈ On) → ((w We A ∧ (¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅ ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅)) → (((F ‘a) = r ∧ (F ‘b) = s) → (rRs ∨ r = s ∨ sRr)))))
48	47	pm2.43i 58	. . . . . . . . . . . . . . 15 ⊢ ((a ∈ On ∧ b ∈ On) → ((w We A ∧ (¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅ ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅)) → (((F ‘a) = r ∧ (F ‘b) = s) → (rRs ∨ r = s ∨ sRr))))
49	16, 48	syl6 23	. . . . . . . . . . . . . 14 ⊢ (x ∈ On → ((a ∈ x ∧ b ∈ x) → ((w We A ∧ (¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅ ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅)) → (((F ‘a) = r ∧ (F ‘b) = s) → (rRs ∨ r = s ∨ sRr)))))
50	49	exp4a 295	. . . . . . . . . . . . 13 ⊢ (x ∈ On → ((a ∈ x ∧ b ∈ x) → (w We A → ((¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅ ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅) → (((F ‘a) = r ∧ (F ‘b) = s) → (rRs ∨ r = s ∨ sRr))))))
51	50	com3r 35	. . . . . . . . . . . 12 ⊢ (w We A → (x ∈ On → ((a ∈ x ∧ b ∈ x) → ((¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅ ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅) → (((F ‘a) = r ∧ (F ‘b) = s) → (rRs ∨ r = s ∨ sRr))))))
52	51	imp 277	. . . . . . . . . . 11 ⊢ ((w We A ∧ x ∈ On) → ((a ∈ x ∧ b ∈ x) → ((¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅ ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅) → (((F ‘a) = r ∧ (F ‘b) = s) → (rRs ∨ r = s ∨ sRr)))))
53	52	a2d 15	. . . . . . . . . 10 ⊢ ((w We A ∧ x ∈ On) → (((a ∈ x ∧ b ∈ x) → (¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅ ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅)) → ((a ∈ x ∧ b ∈ x) → (((F ‘a) = r ∧ (F ‘b) = s) → (rRs ∨ r = s ∨ sRr)))))
54	7	cleq1i 1108	. . . . . . . . . . . . 13 ⊢ (H = ∅ ↔ {z ∈ A∣∀g ∈ (F “ y)gRz} = ∅)
55	54	negbii 162	. . . . . . . . . . . 12 ⊢ (¬ H = ∅ ↔ ¬ {z ∈ A∣∀g ∈ (F “ y)gRz} = ∅)
56	55	biral 1223	. . . . . . . . . . 11 ⊢ (∀y ∈ x ¬ H = ∅ ↔ ∀y ∈ x ¬ {z ∈ A∣∀g ∈ (F “ y)gRz} = ∅)
57		imaeq2 2603	. . . . . . . . . . . . . . . . 17 ⊢ (y = a → (F “ y) = (F “ a))
58		raleq 1324	. . . . . . . . . . . . . . . . 17 ⊢ ((F “ y) = (F “ a) → (∀g ∈ (F “ y)gRz ↔ ∀g ∈ (F “ a)gRz))
59	57, 58	syl 12	. . . . . . . . . . . . . . . 16 ⊢ (y = a → (∀g ∈ (F “ y)gRz ↔ ∀g ∈ (F “ a)gRz))
60	59	birabsdv 1344	. . . . . . . . . . . . . . 15 ⊢ (y = a → {z ∈ A∣∀g ∈ (F “ y)gRz} = {z ∈ A∣∀g ∈ (F “ a)gRz})
61	60	cleq1d 1109	. . . . . . . . . . . . . 14 ⊢ (y = a → ({z ∈ A∣∀g ∈ (F “ y)gRz} = ∅ ↔ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅))
62	61	negbid 463	. . . . . . . . . . . . 13 ⊢ (y = a → (¬ {z ∈ A∣∀g ∈ (F “ y)gRz} = ∅ ↔ ¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅))
63	62	rcla4v 1402	. . . . . . . . . . . 12 ⊢ (∀y ∈ x ¬ {z ∈ A∣∀g ∈ (F “ y)gRz} = ∅ → (a ∈ x → ¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅))
64		imaeq2 2603	. . . . . . . . . . . . . . . . 17 ⊢ (y = b → (F “ y) = (F “ b))
65		raleq 1324	. . . . . . . . . . . . . . . . 17 ⊢ ((F “ y) = (F “ b) → (∀g ∈ (F “ y)gRz ↔ ∀g ∈ (F “ b)gRz))
66	64, 65	syl 12	. . . . . . . . . . . . . . . 16 ⊢ (y = b → (∀g ∈ (F “ y)gRz ↔ ∀g ∈ (F “ b)gRz))
67	66	birabsdv 1344	. . . . . . . . . . . . . . 15 ⊢ (y = b → {z ∈ A∣∀g ∈ (F “ y)gRz} = {z ∈ A∣∀g ∈ (F “ b)gRz})
68	67	cleq1d 1109	. . . . . . . . . . . . . 14 ⊢ (y = b → ({z ∈ A∣∀g ∈ (F “ y)gRz} = ∅ ↔ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅))
69	68	negbid 463	. . . . . . . . . . . . 13 ⊢ (y = b → (¬ {z ∈ A∣∀g ∈ (F “ y)gRz} = ∅ ↔ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅))
70	69	rcla4v 1402	. . . . . . . . . . . 12 ⊢ (∀y ∈ x ¬ {z ∈ A∣∀g ∈ (F “ y)gRz} = ∅ → (b ∈ x → ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅))
71	63, 70	anim12d 431	. . . . . . . . . . 11 ⊢ (∀y ∈ x ¬ {z ∈ A∣∀g ∈ (F “ y)gRz} = ∅ → ((a ∈ x ∧ b ∈ x) → (¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅ ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅)))
72	56, 71	sylbi 174	. . . . . . . . . 10 ⊢ (∀y ∈ x ¬ H = ∅ → ((a ∈ x ∧ b ∈ x) → (¬ {z ∈ A∣∀g ∈ (F “ a)gRz} = ∅ ∧ ¬ {z ∈ A∣∀g ∈ (F “ b)gRz} = ∅)))
73	53, 72	syl5 22	. . . . . . . . 9 ⊢ ((w We A ∧ x ∈ On) → (∀y ∈ x ¬ H = ∅ → ((a ∈ x ∧ b ∈ x) → (((F ‘a) = r ∧ (F ‘b) = s) → (rRs ∨ r = s ∨ sRr)))))
74	73	imp4b 283	. . . . . . . 8 ⊢ (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → (((a ∈ x ∧ b ∈ x) ∧ ((F ‘a) = r ∧ (F ‘b) = s)) → (rRs ∨ r = s ∨ sRr)))
75	74	19.23advv 955	. . . . . . 7 ⊢ (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → (∃a∃b((a ∈ x ∧ b ∈ x) ∧ ((F ‘a) = r ∧ (F ‘b) = s)) → (rRs ∨ r = s ∨ sRr)))
76	2, 3	tfr1 2962	. . . . . . . . . 10 ⊢ F Fn On
77		fnfun 2721	. . . . . . . . . 10 ⊢ (F Fn On → Fun F)
78	76, 77	ax-mp 6	. . . . . . . . 9 ⊢ Fun F
79		fvelima 2859	. . . . . . . . . . . 12 ⊢ ((Fun F ∧ r ∈ (F “ x)) → ∃a ∈ x (F ‘a) = r)
80		df-rex 1206	. . . . . . . . . . . 12 ⊢ (∃a ∈ x (F ‘a) = r ↔ ∃a(a ∈ x ∧ (F ‘a) = r))
81	79, 80	sylib 173	. . . . . . . . . . 11 ⊢ ((Fun F ∧ r ∈ (F “ x)) → ∃a(a ∈ x ∧ (F ‘a) = r))
82	81	exp 291	. . . . . . . . . 10 ⊢ (Fun F → (r ∈ (F “ x) → ∃a(a ∈ x ∧ (F ‘a) = r)))
83		fvelima 2859	. . . . . . . . . . . 12 ⊢ ((Fun F ∧ s ∈ (F “ x)) → ∃b ∈ x (F ‘b) = s)
84		df-rex 1206	. . . . . . . . . . . 12 ⊢ (∃b ∈ x (F ‘b) = s ↔ ∃b(b ∈ x ∧ (F ‘b) = s))
85	83, 84	sylib 173	. . . . . . . . . . 11 ⊢ ((Fun F ∧ s ∈ (F “ x)) → ∃b(b ∈ x ∧ (F ‘b) = s))
86	85	exp 291	. . . . . . . . . 10 ⊢ (Fun F → (s ∈ (F “ x) → ∃b(b ∈ x ∧ (F ‘b) = s)))
87	82, 86	anim12d 431	. . . . . . . . 9 ⊢ (Fun F → ((r ∈ (F “ x) ∧ s ∈ (F “ x)) → (∃a(a ∈ x ∧ (F ‘a) = r) ∧ ∃b(b ∈ x ∧ (F ‘b) = s))))
88	78, 87	ax-mp 6	. . . . . . . 8 ⊢ ((r ∈ (F “ x) ∧ s ∈ (F “ x)) → (∃a(a ∈ x ∧ (F ‘a) = r) ∧ ∃b(b ∈ x ∧ (F ‘b) = s)))
89		an4 388	. . . . . . . . . 10 ⊢ (((a ∈ x ∧ b ∈ x) ∧ ((F ‘a) = r ∧ (F ‘b) = s)) ↔ ((a ∈ x ∧ (F ‘a) = r) ∧ (b ∈ x ∧ (F ‘b) = s)))
90	89	bi2ex 734	. . . . . . . . 9 ⊢ (∃a∃b((a ∈ x ∧ b ∈ x) ∧ ((F ‘a) = r ∧ (F ‘b) = s)) ↔ ∃a∃b((a ∈ x ∧ (F ‘a) = r) ∧ (b ∈ x ∧ (F ‘b) = s)))
91		eeanv 980	. . . . . . . . 9 ⊢ (∃a∃b((a ∈ x ∧ (F ‘a) = r) ∧ (b ∈ x ∧ (F ‘b) = s)) ↔ (∃a(a ∈ x ∧ (F ‘a) = r) ∧ ∃b(b ∈ x ∧ (F ‘b) = s)))
92	90, 91	bitr 151	. . . . . . . 8 ⊢ (∃a∃b((a ∈ x ∧ b ∈ x) ∧ ((F ‘a) = r ∧ (F ‘b) = s)) ↔ (∃a(a ∈ x ∧ (F ‘a) = r) ∧ ∃b(b ∈ x ∧ (F ‘b) = s)))
93	88, 92	sylibr 175	. . . . . . 7 ⊢ ((r ∈ (F “ x) ∧ s ∈ (F “ x)) → ∃a∃b((a ∈ x ∧ b ∈ x) ∧ ((F ‘a) = r ∧ (F ‘b) = s)))
94	75, 93	syl5 22	. . . . . 6 ⊢ (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → ((r ∈ (F “ x) ∧ s ∈ (F “ x)) → (rRs ∨ r = s ∨ sRr)))
95	94	19.21aivv 944	. . . . 5 ⊢ (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → ∀r∀s((r ∈ (F “ x) ∧ s ∈ (F “ x)) → (rRs ∨ r = s ∨ sRr)))
96		r2al 1231	. . . . 5 ⊢ (∀r ∈ (F “ x)∀s ∈ (F “ x)(rRs ∨ r = s ∨ sRr) ↔ ∀r∀s((r ∈ (F “ x) ∧ s ∈ (F “ x)) → (rRs ∨ r = s ∨ sRr)))
97	95, 96	sylibr 175	. . . 4 ⊢ (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → ∀r ∈ (F “ x)∀s ∈ (F “ x)(rRs ∨ r = s ∨ sRr))
98	97	a1i 7	. . 3 ⊢ (R Po A → (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → ∀r ∈ (F “ x)∀s ∈ (F “ x)(rRs ∨ r = s ∨ sRr)))
99	11, 98	jcad 455	. 2 ⊢ (R Po A → (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → (R Po (F “ x) ∧ ∀r ∈ (F “ x)∀s ∈ (F “ x)(rRs ∨ r = s ∨ sRr))))
100		df-so 2138	. 2 ⊢ (R Or (F “ x) ↔ (R Po (F “ x) ∧ ∀r ∈ (F “ x)∀s ∈ (F “ x)(rRs ∨ r = s ∨ sRr)))
101	99, 100	syl6ibr 186	1 ⊢ (R Po A → (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → R Or (F “ x)))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∧ wa 196 ∨ w3o 580 ∀wal 672 ∃wex 678 = weq 797 ∈ wel 803 {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 We wwe 2062 Ord word 2198 Oncon0 2199 ran crn 2411 ↾ cres 2412 “ cima 2413 Fun wfun 2416 Fn wfn 2417 ‘cfv 2422

This theorem is referenced by: zornlem7 3609

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-nul 1708 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-suc 2205 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-fv 2438

metamath.org