Theorem poseq 32649

Description: A partial ordering of sequences of ordinals. (Contributed by Scott Fenton, 8-Jun-2011.)

Hypotheses

Ref	Expression
poseq.1	⊢ 𝑅 Po (𝐴 ∪ {∅})
poseq.2	⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴}
poseq.3	⊢ 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))}

Assertion

Ref	Expression
poseq	⊢ 𝑆 Po 𝐹

Distinct variable groups:   𝐴,𝑓,𝑥   𝑓,𝑔,𝑦,𝑥   𝑓,𝐹,𝑔,𝑥   𝑅,𝑓,𝑔,𝑥

Allowed substitution hints:   𝐴(𝑦,𝑔)   𝑅(𝑦)   𝑆(𝑥,𝑦,𝑓,𝑔)   𝐹(𝑦)

Proof of Theorem poseq

Dummy variables 𝑏 𝑎 𝑐 𝑡 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		poseq.1	. . . . . . . . . . . 12 ⊢ 𝑅 Po (𝐴 ∪ {∅})
2		poseq.2	. . . . . . . . . . . . . 14 ⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴}
3		feq2 6324	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑏 → (𝑓:𝑥⟶𝐴 ↔ 𝑓:𝑏⟶𝐴))
4	3	cbvrexv 3379	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥 ∈ On 𝑓:𝑥⟶𝐴 ↔ ∃𝑏 ∈ On 𝑓:𝑏⟶𝐴)
5	4	abbii 2839	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏⟶𝐴}
6	2, 5	eqtri 2797	. . . . . . . . . . . . 13 ⊢ 𝐹 = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏⟶𝐴}
7	6	orderseqlem 32648	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝐹 → (𝑎‘𝑥) ∈ (𝐴 ∪ {∅}))
8		poirr 5334	. . . . . . . . . . . 12 ⊢ ((𝑅 Po (𝐴 ∪ {∅}) ∧ (𝑎‘𝑥) ∈ (𝐴 ∪ {∅})) → ¬ (𝑎‘𝑥)𝑅(𝑎‘𝑥))
9	1, 7, 8	sylancr 579	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝐹 → ¬ (𝑎‘𝑥)𝑅(𝑎‘𝑥))
10	9	intnand 481	. . . . . . . . . 10 ⊢ (𝑎 ∈ 𝐹 → ¬ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
11	10	adantr 473	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑥 ∈ On) → ¬ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
12	11	nrexdv 3210	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐹 → ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
13	12	adantr 473	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
14		imnan 391	. . . . . . 7 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))) ↔ ¬ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
15	13, 14	mpbi 222	. . . . . 6 ⊢ ¬ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
16		vex 3413	. . . . . . 7 ⊢ 𝑎 ∈ V
17		eleq1w 2843	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → (𝑓 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹))
18	17	anbi1d 621	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹)))
19		fveq1 6496	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑦) = (𝑎‘𝑦))
20	19	eqeq1d 2775	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑔‘𝑦)))
21	20	ralbidv 3142	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦)))
22		fveq1 6496	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑥) = (𝑎‘𝑥))
23	22	breq1d 4936	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))
24	21, 23	anbi12d 622	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))))
25	24	rexbidv 3237	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))))
26	18, 25	anbi12d 622	. . . . . . 7 ⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))))
27		eleq1w 2843	. . . . . . . . 9 ⊢ (𝑔 = 𝑎 → (𝑔 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹))
28	27	anbi2d 620	. . . . . . . 8 ⊢ (𝑔 = 𝑎 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹)))
29		fveq1 6496	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑦) = (𝑎‘𝑦))
30	29	eqeq2d 2783	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑎 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑎‘𝑦)))
31	30	ralbidv 3142	. . . . . . . . . 10 ⊢ (𝑔 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦)))
32		fveq1 6496	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑥) = (𝑎‘𝑥))
33	32	breq2d 4938	. . . . . . . . . 10 ⊢ (𝑔 = 𝑎 → ((𝑎‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
34	31, 33	anbi12d 622	. . . . . . . . 9 ⊢ (𝑔 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
35	34	rexbidv 3237	. . . . . . . 8 ⊢ (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
36	28, 35	anbi12d 622	. . . . . . 7 ⊢ (𝑔 = 𝑎 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))))
37		poseq.3	. . . . . . 7 ⊢ 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))}
38	16, 16, 26, 36, 37	brab 5281	. . . . . 6 ⊢ (𝑎𝑆𝑎 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
39	15, 38	mtbir 315	. . . . 5 ⊢ ¬ 𝑎𝑆𝑎
40		vex 3413	. . . . . . . 8 ⊢ 𝑏 ∈ V
41		raleq 3340	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦)))
42		fveq2 6497	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑓‘𝑥) = (𝑓‘𝑧))
43		fveq2 6497	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑔‘𝑥) = (𝑔‘𝑧))
44	42, 43	breq12d 4939	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑓‘𝑧)𝑅(𝑔‘𝑧)))
45	41, 44	anbi12d 622	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧))))
46	45	cbvrexv 3379	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧)))
47	20	ralbidv 3142	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦)))
48		fveq1 6496	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑧) = (𝑎‘𝑧))
49	48	breq1d 4936	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑧)𝑅(𝑔‘𝑧) ↔ (𝑎‘𝑧)𝑅(𝑔‘𝑧)))
50	47, 49	anbi12d 622	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))))
51	50	rexbidv 3237	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))))
52	46, 51	syl5bb 275	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))))
53	18, 52	anbi12d 622	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧)))))
54		eleq1w 2843	. . . . . . . . . 10 ⊢ (𝑔 = 𝑏 → (𝑔 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹))
55	54	anbi2d 620	. . . . . . . . 9 ⊢ (𝑔 = 𝑏 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹)))
56		fveq1 6496	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑦) = (𝑏‘𝑦))
57	56	eqeq2d 2783	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑏 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑏‘𝑦)))
58	57	ralbidv 3142	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑏 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦)))
59		fveq1 6496	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑧) = (𝑏‘𝑧))
60	59	breq2d 4938	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑏 → ((𝑎‘𝑧)𝑅(𝑔‘𝑧) ↔ (𝑎‘𝑧)𝑅(𝑏‘𝑧)))
61	58, 60	anbi12d 622	. . . . . . . . . 10 ⊢ (𝑔 = 𝑏 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))))
62	61	rexbidv 3237	. . . . . . . . 9 ⊢ (𝑔 = 𝑏 → (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))))
63	55, 62	anbi12d 622	. . . . . . . 8 ⊢ (𝑔 = 𝑏 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)))))
64	16, 40, 53, 63, 37	brab 5281	. . . . . . 7 ⊢ (𝑎𝑆𝑏 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))))
65		vex 3413	. . . . . . . 8 ⊢ 𝑐 ∈ V
66		eleq1w 2843	. . . . . . . . . 10 ⊢ (𝑓 = 𝑏 → (𝑓 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹))
67	66	anbi1d 621	. . . . . . . . 9 ⊢ (𝑓 = 𝑏 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹)))
68		raleq 3340	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦)))
69		fveq2 6497	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → (𝑓‘𝑥) = (𝑓‘𝑤))
70		fveq2 6497	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → (𝑔‘𝑥) = (𝑔‘𝑤))
71	69, 70	breq12d 4939	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑓‘𝑤)𝑅(𝑔‘𝑤)))
72	68, 71	anbi12d 622	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤))))
73	72	cbvrexv 3379	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤)))
74		fveq1 6496	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑦) = (𝑏‘𝑦))
75	74	eqeq1d 2775	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑔‘𝑦)))
76	75	ralbidv 3142	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦)))
77		fveq1 6496	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑤) = (𝑏‘𝑤))
78	77	breq1d 4936	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑤)𝑅(𝑔‘𝑤) ↔ (𝑏‘𝑤)𝑅(𝑔‘𝑤)))
79	76, 78	anbi12d 622	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑏 → ((∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤)) ↔ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))))
80	79	rexbidv 3237	. . . . . . . . . 10 ⊢ (𝑓 = 𝑏 → (∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))))
81	73, 80	syl5bb 275	. . . . . . . . 9 ⊢ (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))))
82	67, 81	anbi12d 622	. . . . . . . 8 ⊢ (𝑓 = 𝑏 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤)))))
83		eleq1w 2843	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → (𝑔 ∈ 𝐹 ↔ 𝑐 ∈ 𝐹))
84	83	anbi2d 620	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))
85		fveq1 6496	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑐 → (𝑔‘𝑦) = (𝑐‘𝑦))
86	85	eqeq2d 2783	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑐 → ((𝑏‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑐‘𝑦)))
87	86	ralbidv 3142	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)))
88		fveq1 6496	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑐 → (𝑔‘𝑤) = (𝑐‘𝑤))
89	88	breq2d 4938	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → ((𝑏‘𝑤)𝑅(𝑔‘𝑤) ↔ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))
90	87, 89	anbi12d 622	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → ((∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤)) ↔ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
91	90	rexbidv 3237	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → (∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
92	84, 91	anbi12d 622	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))))
93	40, 65, 82, 92, 37	brab 5281	. . . . . . 7 ⊢ (𝑏𝑆𝑐 ↔ ((𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
94		simplll 763	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑎 ∈ 𝐹)
95		simplrr 766	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑐 ∈ 𝐹)
96		an4 644	. . . . . . . . . . . . 13 ⊢ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
97	96	2rexbii 3190	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ ∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
98		reeanv 3303	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
99	97, 98	bitri 267	. . . . . . . . . . 11 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
100		eloni 6037	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ On → Ord 𝑧)
101		eloni 6037	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ On → Ord 𝑤)
102		ordtri3or 6059	. . . . . . . . . . . . . 14 ⊢ ((Ord 𝑧 ∧ Ord 𝑤) → (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))
103	100, 101, 102	syl2an 587	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))
104		simp1l 1178	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑧 ∈ On)
105		onelss 6069	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ On → (𝑧 ∈ 𝑤 → 𝑧 ⊆ 𝑤))
106	105	imp 398	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤 ∈ On ∧ 𝑧 ∈ 𝑤) → 𝑧 ⊆ 𝑤)
107	106	adantll 702	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤) → 𝑧 ⊆ 𝑤)
108		ssralv 3918	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ⊆ 𝑤 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦)))
109	108	anim2d 603	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ⊆ 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦))))
110		r19.26 3115	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦)))
111	109, 110	syl6ibr 244	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ⊆ 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦))))
112		eqtr 2794	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) → (𝑎‘𝑦) = (𝑐‘𝑦))
113	112	ralimi 3105	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦))
114	111, 113	syl6 35	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ⊆ 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
115	107, 114	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤) → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
116	115	adantrd 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
117	116	3impia 1098	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦))
118		fveq2 6497	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑧 → (𝑏‘𝑦) = (𝑏‘𝑧))
119		fveq2 6497	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑧 → (𝑐‘𝑦) = (𝑐‘𝑧))
120	118, 119	eqeq12d 2788	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑧 → ((𝑏‘𝑦) = (𝑐‘𝑦) ↔ (𝑏‘𝑧) = (𝑐‘𝑧)))
121	120	rspcv 3526	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ 𝑤 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → (𝑏‘𝑧) = (𝑐‘𝑧)))
122		breq2 4930	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏‘𝑧) = (𝑐‘𝑧) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ↔ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
123	122	biimpd 221	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏‘𝑧) = (𝑐‘𝑧) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
124	121, 123	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ 𝑤 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))))
125	124	com3l 89	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) → (𝑧 ∈ 𝑤 → (𝑎‘𝑧)𝑅(𝑐‘𝑧))))
126	125	imp 398	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) → (𝑧 ∈ 𝑤 → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
127	126	ad2ant2lr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (𝑧 ∈ 𝑤 → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
128	127	impcom 399	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))
129	128	3adant1 1111	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))
130		raleq 3340	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑧 → (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
131		fveq2 6497	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑧 → (𝑎‘𝑡) = (𝑎‘𝑧))
132		fveq2 6497	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑧 → (𝑐‘𝑡) = (𝑐‘𝑧))
133	131, 132	breq12d 4939	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑧 → ((𝑎‘𝑡)𝑅(𝑐‘𝑡) ↔ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
134	130, 133	anbi12d 622	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑧 → ((∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧))))
135	134	rspcev 3530	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ On ∧ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
136	104, 117, 129, 135	syl12anc 825	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
137	136	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
138	137	3exp 1100	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ∈ 𝑤 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
139	2	orderseqlem 32648	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ 𝐹 → (𝑎‘𝑧) ∈ (𝐴 ∪ {∅}))
140	139	ad2antrr 714	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (𝑎‘𝑧) ∈ (𝐴 ∪ {∅}))
141	2	orderseqlem 32648	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ∈ 𝐹 → (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}))
142	141	ad2antlr 715	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}))
143	2	orderseqlem 32648	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ 𝐹 → (𝑐‘𝑧) ∈ (𝐴 ∪ {∅}))
144	143	ad2antll 717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (𝑐‘𝑧) ∈ (𝐴 ∪ {∅}))
145	140, 142, 144	3jca 1109	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ((𝑎‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐‘𝑧) ∈ (𝐴 ∪ {∅})))
146		potr 5335	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Po (𝐴 ∪ {∅}) ∧ ((𝑎‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐‘𝑧) ∈ (𝐴 ∪ {∅}))) → (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
147	1, 145, 146	sylancr 579	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
148	147	impcom 399	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹))) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))
149	113, 148	anim12i 604	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))) → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
150	149	anassrs 460	. . . . . . . . . . . . . . . . . 18 ⊢ (((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹))) → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
151	150, 135	sylan2 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ On ∧ ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
152	151	exp32 413	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ On → ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))))
153		raleq 3340	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑤 → (∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)))
154	153	anbi2d 620	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦))))
155	110, 154	syl5bb 275	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑤 → (∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦))))
156		fveq2 6497	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑤 → (𝑏‘𝑧) = (𝑏‘𝑤))
157		fveq2 6497	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑤 → (𝑐‘𝑧) = (𝑐‘𝑤))
158	156, 157	breq12d 4939	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → ((𝑏‘𝑧)𝑅(𝑐‘𝑧) ↔ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))
159	158	anbi2d 620	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑤 → (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) ↔ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
160	155, 159	anbi12d 622	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑤 → ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) ↔ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))))
161	160	imbi1d 334	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑤 → (((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))) ↔ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
162	152, 161	syl5ibcom 237	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ On → (𝑧 = 𝑤 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
163	162	adantr 473	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 = 𝑤 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
164		simp1r 1179	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑤 ∈ On)
165		onelss 6069	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ On → (𝑤 ∈ 𝑧 → 𝑤 ⊆ 𝑧))
166	165	imp 398	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ 𝑧) → 𝑤 ⊆ 𝑧)
167	166	adantlr 703	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧) → 𝑤 ⊆ 𝑧)
168		ssralv 3918	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ⊆ 𝑧 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦)))
169	168	anim1d 602	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ⊆ 𝑧 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦))))
170		r19.26 3115	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ 𝑤 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)))
171	112	ralimi 3105	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ 𝑤 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦))
172	170, 171	sylbir 227	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦))
173	169, 172	syl6 35	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ⊆ 𝑧 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
174	173	adantrd 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ⊆ 𝑧 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
175	167, 174	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
176	175	3impia 1098	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦))
177		fveq2 6497	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑤 → (𝑎‘𝑦) = (𝑎‘𝑤))
178		fveq2 6497	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑤 → (𝑏‘𝑦) = (𝑏‘𝑤))
179	177, 178	eqeq12d 2788	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑤 → ((𝑎‘𝑦) = (𝑏‘𝑦) ↔ (𝑎‘𝑤) = (𝑏‘𝑤)))
180	179	rspcv 3526	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ 𝑧 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑤) = (𝑏‘𝑤)))
181		breq1 4929	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎‘𝑤) = (𝑏‘𝑤) → ((𝑎‘𝑤)𝑅(𝑐‘𝑤) ↔ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))
182	181	biimprd 240	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎‘𝑤) = (𝑏‘𝑤) → ((𝑏‘𝑤)𝑅(𝑐‘𝑤) → (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
183	180, 182	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ 𝑧 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → ((𝑏‘𝑤)𝑅(𝑐‘𝑤) → (𝑎‘𝑤)𝑅(𝑐‘𝑤))))
184	183	com3l 89	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → ((𝑏‘𝑤)𝑅(𝑐‘𝑤) → (𝑤 ∈ 𝑧 → (𝑎‘𝑤)𝑅(𝑐‘𝑤))))
185	184	imp 398	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)) → (𝑤 ∈ 𝑧 → (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
186	185	ad2ant2rl 737	. . . . . . . . . . . . . . . . . . 19 ⊢ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (𝑤 ∈ 𝑧 → (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
187	186	impcom 399	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑤)𝑅(𝑐‘𝑤))
188	187	3adant1 1111	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑤)𝑅(𝑐‘𝑤))
189		raleq 3340	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑤 → (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
190		fveq2 6497	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑤 → (𝑎‘𝑡) = (𝑎‘𝑤))
191		fveq2 6497	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑤 → (𝑐‘𝑡) = (𝑐‘𝑤))
192	190, 191	breq12d 4939	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑤 → ((𝑎‘𝑡)𝑅(𝑐‘𝑡) ↔ (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
193	189, 192	anbi12d 622	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑤 → ((∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)) ↔ (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑤)𝑅(𝑐‘𝑤))))
194	193	rspcev 3530	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ On ∧ (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑤)𝑅(𝑐‘𝑤))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
195	164, 176, 188, 194	syl12anc 825	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
196	195	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
197	196	3exp 1100	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑤 ∈ 𝑧 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
198	138, 163, 197	3jaod 1409	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → ((𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
199	103, 198	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))))
200	199	rexlimivv 3232	. . . . . . . . . . 11 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
201	99, 200	sylbir 227	. . . . . . . . . 10 ⊢ ((∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
202	201	impcom 399	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
203	94, 95, 202	jca31 507	. . . . . . . 8 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
204	203	an4s 648	. . . . . . 7 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))) ∧ ((𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
205	64, 93, 204	syl2anb 589	. . . . . 6 ⊢ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
206		raleq 3340	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦)))
207		fveq2 6497	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → (𝑓‘𝑥) = (𝑓‘𝑡))
208		fveq2 6497	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → (𝑔‘𝑥) = (𝑔‘𝑡))
209	207, 208	breq12d 4939	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑓‘𝑡)𝑅(𝑔‘𝑡)))
210	206, 209	anbi12d 622	. . . . . . . . . 10 ⊢ (𝑥 = 𝑡 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡))))
211	210	cbvrexv 3379	. . . . . . . . 9 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡)))
212	20	ralbidv 3142	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦)))
213		fveq1 6496	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑡) = (𝑎‘𝑡))
214	213	breq1d 4936	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑡)𝑅(𝑔‘𝑡) ↔ (𝑎‘𝑡)𝑅(𝑔‘𝑡)))
215	212, 214	anbi12d 622	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡)) ↔ (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))))
216	215	rexbidv 3237	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → (∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))))
217	211, 216	syl5bb 275	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))))
218	18, 217	anbi12d 622	. . . . . . 7 ⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡)))))
219	83	anbi2d 620	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))
220	85	eqeq2d 2783	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑐‘𝑦)))
221	220	ralbidv 3142	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦)))
222		fveq1 6496	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → (𝑔‘𝑡) = (𝑐‘𝑡))
223	222	breq2d 4938	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → ((𝑎‘𝑡)𝑅(𝑔‘𝑡) ↔ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
224	221, 223	anbi12d 622	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → ((∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡)) ↔ (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
225	224	rexbidv 3237	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
226	219, 225	anbi12d 622	. . . . . . 7 ⊢ (𝑔 = 𝑐 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))))
227	16, 65, 218, 226, 37	brab 5281	. . . . . 6 ⊢ (𝑎𝑆𝑐 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
228	205, 227	sylibr 226	. . . . 5 ⊢ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)
229	39, 228	pm3.2i 463	. . . 4 ⊢ (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐))
230	229	a1i 11	. . 3 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) → (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
231	230	rgen3 3149	. 2 ⊢ ∀𝑎 ∈ 𝐹 ∀𝑏 ∈ 𝐹 ∀𝑐 ∈ 𝐹 (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐))
232		df-po 5323	. 2 ⊢ (𝑆 Po 𝐹 ↔ ∀𝑎 ∈ 𝐹 ∀𝑏 ∈ 𝐹 ∀𝑐 ∈ 𝐹 (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
233	231, 232	mpbir 223	1 ⊢ 𝑆 Po 𝐹

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 387   ∨ w3o 1068   ∧ w3a 1069   = wceq 1508   ∈ wcel 2051  {cab 2753  ∀wral 3083  ∃wrex 3084   ∪ cun 3822   ⊆ wss 3824  ∅c0 4173  {csn 4436   class class class wbr 4926  {copab 4988   Po wpo 5321  Ord word 6026  Oncon0 6027  ⟶wf 6182  ‘cfv 6186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-ral 3088  df-rex 3089  df-rab 3092  df-v 3412  df-sbc 3677  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-pss 3840  df-nul 4174  df-if 4346  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-br 4927  df-opab 4989  df-tr 5028  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-we 5365  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-ord 6030  df-on 6031  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-fv 6194

This theorem is referenced by:  soseq  32650