Theorem poseq 30994

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 5940	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑏 → (𝑓:𝑥⟶𝐴 ↔ 𝑓:𝑏⟶𝐴))
4	3	cbvrexv 3148	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥 ∈ On 𝑓:𝑥⟶𝐴 ↔ ∃𝑏 ∈ On 𝑓:𝑏⟶𝐴)
5	4	abbii 2726	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏⟶𝐴}
6	2, 5	eqtri 2632	. . . . . . . . . . . . 13 ⊢ 𝐹 = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏⟶𝐴}
7	6	orderseqlem 30993	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝐹 → (𝑎‘𝑥) ∈ (𝐴 ∪ {∅}))
8		poirr 4970	. . . . . . . . . . . 12 ⊢ ((𝑅 Po (𝐴 ∪ {∅}) ∧ (𝑎‘𝑥) ∈ (𝐴 ∪ {∅})) → ¬ (𝑎‘𝑥)𝑅(𝑎‘𝑥))
9	1, 7, 8	sylancr 694	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝐹 → ¬ (𝑎‘𝑥)𝑅(𝑎‘𝑥))
10	9	intnand 953	. . . . . . . . . 10 ⊢ (𝑎 ∈ 𝐹 → ¬ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
11	10	adantr 480	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑥 ∈ On) → ¬ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
12	11	nrexdv 2984	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐹 → ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
13	12	adantr 480	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
14		imnan 437	. . . . . . 7 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))) ↔ ¬ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
15	13, 14	mpbi 219	. . . . . 6 ⊢ ¬ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
16		vex 3176	. . . . . . 7 ⊢ 𝑎 ∈ V
17		eleq1 2676	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → (𝑓 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹))
18	17	anbi1d 737	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹)))
19		fveq1 6102	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑦) = (𝑎‘𝑦))
20	19	eqeq1d 2612	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑔‘𝑦)))
21	20	ralbidv 2969	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦)))
22		fveq1 6102	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑥) = (𝑎‘𝑥))
23	22	breq1d 4593	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))
24	21, 23	anbi12d 743	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))))
25	24	rexbidv 3034	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))))
26	18, 25	anbi12d 743	. . . . . . 7 ⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))))
27		eleq1 2676	. . . . . . . . 9 ⊢ (𝑔 = 𝑎 → (𝑔 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹))
28	27	anbi2d 736	. . . . . . . 8 ⊢ (𝑔 = 𝑎 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹)))
29		fveq1 6102	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑦) = (𝑎‘𝑦))
30	29	eqeq2d 2620	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑎 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑎‘𝑦)))
31	30	ralbidv 2969	. . . . . . . . . 10 ⊢ (𝑔 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦)))
32		fveq1 6102	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑥) = (𝑎‘𝑥))
33	32	breq2d 4595	. . . . . . . . . 10 ⊢ (𝑔 = 𝑎 → ((𝑎‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
34	31, 33	anbi12d 743	. . . . . . . . 9 ⊢ (𝑔 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
35	34	rexbidv 3034	. . . . . . . 8 ⊢ (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
36	28, 35	anbi12d 743	. . . . . . 7 ⊢ (𝑔 = 𝑎 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))))
37		poseq.3	. . . . . . 7 ⊢ 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))}
38	16, 16, 26, 36, 37	brab 4923	. . . . . 6 ⊢ (𝑎𝑆𝑎 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
39	15, 38	mtbir 312	. . . . 5 ⊢ ¬ 𝑎𝑆𝑎
40		vex 3176	. . . . . . . 8 ⊢ 𝑏 ∈ V
41		raleq 3115	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦)))
42		fveq2 6103	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑓‘𝑥) = (𝑓‘𝑧))
43		fveq2 6103	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑔‘𝑥) = (𝑔‘𝑧))
44	42, 43	breq12d 4596	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑓‘𝑧)𝑅(𝑔‘𝑧)))
45	41, 44	anbi12d 743	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧))))
46	45	cbvrexv 3148	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧)))
47	20	ralbidv 2969	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦)))
48		fveq1 6102	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑧) = (𝑎‘𝑧))
49	48	breq1d 4593	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑧)𝑅(𝑔‘𝑧) ↔ (𝑎‘𝑧)𝑅(𝑔‘𝑧)))
50	47, 49	anbi12d 743	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))))
51	50	rexbidv 3034	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))))
52	46, 51	syl5bb 271	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))))
53	18, 52	anbi12d 743	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧)))))
54		eleq1 2676	. . . . . . . . . 10 ⊢ (𝑔 = 𝑏 → (𝑔 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹))
55	54	anbi2d 736	. . . . . . . . 9 ⊢ (𝑔 = 𝑏 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹)))
56		fveq1 6102	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑦) = (𝑏‘𝑦))
57	56	eqeq2d 2620	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑏 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑏‘𝑦)))
58	57	ralbidv 2969	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑏 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦)))
59		fveq1 6102	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑧) = (𝑏‘𝑧))
60	59	breq2d 4595	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑏 → ((𝑎‘𝑧)𝑅(𝑔‘𝑧) ↔ (𝑎‘𝑧)𝑅(𝑏‘𝑧)))
61	58, 60	anbi12d 743	. . . . . . . . . 10 ⊢ (𝑔 = 𝑏 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))))
62	61	rexbidv 3034	. . . . . . . . 9 ⊢ (𝑔 = 𝑏 → (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))))
63	55, 62	anbi12d 743	. . . . . . . 8 ⊢ (𝑔 = 𝑏 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)))))
64	16, 40, 53, 63, 37	brab 4923	. . . . . . 7 ⊢ (𝑎𝑆𝑏 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))))
65		vex 3176	. . . . . . . 8 ⊢ 𝑐 ∈ V
66		eleq1 2676	. . . . . . . . . 10 ⊢ (𝑓 = 𝑏 → (𝑓 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹))
67	66	anbi1d 737	. . . . . . . . 9 ⊢ (𝑓 = 𝑏 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹)))
68		raleq 3115	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦)))
69		fveq2 6103	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → (𝑓‘𝑥) = (𝑓‘𝑤))
70		fveq2 6103	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → (𝑔‘𝑥) = (𝑔‘𝑤))
71	69, 70	breq12d 4596	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑓‘𝑤)𝑅(𝑔‘𝑤)))
72	68, 71	anbi12d 743	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤))))
73	72	cbvrexv 3148	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤)))
74		fveq1 6102	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑦) = (𝑏‘𝑦))
75	74	eqeq1d 2612	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑔‘𝑦)))
76	75	ralbidv 2969	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦)))
77		fveq1 6102	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑤) = (𝑏‘𝑤))
78	77	breq1d 4593	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑤)𝑅(𝑔‘𝑤) ↔ (𝑏‘𝑤)𝑅(𝑔‘𝑤)))
79	76, 78	anbi12d 743	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑏 → ((∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤)) ↔ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))))
80	79	rexbidv 3034	. . . . . . . . . 10 ⊢ (𝑓 = 𝑏 → (∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))))
81	73, 80	syl5bb 271	. . . . . . . . 9 ⊢ (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))))
82	67, 81	anbi12d 743	. . . . . . . 8 ⊢ (𝑓 = 𝑏 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤)))))
83		eleq1 2676	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → (𝑔 ∈ 𝐹 ↔ 𝑐 ∈ 𝐹))
84	83	anbi2d 736	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))
85		fveq1 6102	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑐 → (𝑔‘𝑦) = (𝑐‘𝑦))
86	85	eqeq2d 2620	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑐 → ((𝑏‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑐‘𝑦)))
87	86	ralbidv 2969	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)))
88		fveq1 6102	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑐 → (𝑔‘𝑤) = (𝑐‘𝑤))
89	88	breq2d 4595	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → ((𝑏‘𝑤)𝑅(𝑔‘𝑤) ↔ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))
90	87, 89	anbi12d 743	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → ((∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤)) ↔ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
91	90	rexbidv 3034	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → (∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
92	84, 91	anbi12d 743	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))))
93	40, 65, 82, 92, 37	brab 4923	. . . . . . 7 ⊢ (𝑏𝑆𝑐 ↔ ((𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
94		simplll 794	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑎 ∈ 𝐹)
95		simplrr 797	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑐 ∈ 𝐹)
96		an4 861	. . . . . . . . . . . . 13 ⊢ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
97	96	2rexbii 3024	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ ∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
98		reeanv 3086	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
99	97, 98	bitri 263	. . . . . . . . . . 11 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
100		eloni 5650	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ On → Ord 𝑧)
101		eloni 5650	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ On → Ord 𝑤)
102		ordtri3or 5672	. . . . . . . . . . . . . 14 ⊢ ((Ord 𝑧 ∧ Ord 𝑤) → (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))
103	100, 101, 102	syl2an 493	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))
104		simp1l 1078	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑧 ∈ On)
105		onelss 5683	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ On → (𝑧 ∈ 𝑤 → 𝑧 ⊆ 𝑤))
106	105	imp 444	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤 ∈ On ∧ 𝑧 ∈ 𝑤) → 𝑧 ⊆ 𝑤)
107	106	adantll 746	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤) → 𝑧 ⊆ 𝑤)
108		ssralv 3629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ⊆ 𝑤 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦)))
109	108	anim2d 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ⊆ 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦))))
110		r19.26 3046	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦)))
111	109, 110	syl6ibr 241	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ⊆ 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦))))
112		eqtr 2629	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) → (𝑎‘𝑦) = (𝑐‘𝑦))
113	112	ralimi 2936	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦))
114	111, 113	syl6 34	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ⊆ 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
115	107, 114	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤) → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
116	115	adantrd 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
117	116	3impia 1253	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦))
118		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑧 → (𝑏‘𝑦) = (𝑏‘𝑧))
119		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑧 → (𝑐‘𝑦) = (𝑐‘𝑧))
120	118, 119	eqeq12d 2625	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑧 → ((𝑏‘𝑦) = (𝑐‘𝑦) ↔ (𝑏‘𝑧) = (𝑐‘𝑧)))
121	120	rspcv 3278	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ 𝑤 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → (𝑏‘𝑧) = (𝑐‘𝑧)))
122		breq2 4587	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏‘𝑧) = (𝑐‘𝑧) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ↔ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
123	122	biimpd 218	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏‘𝑧) = (𝑐‘𝑧) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
124	121, 123	syl6 34	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ 𝑤 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))))
125	124	com3l 87	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) → (𝑧 ∈ 𝑤 → (𝑎‘𝑧)𝑅(𝑐‘𝑧))))
126	125	imp 444	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) → (𝑧 ∈ 𝑤 → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
127	126	ad2ant2lr 780	. . . . . . . . . . . . . . . . . . 19 ⊢ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (𝑧 ∈ 𝑤 → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
128	127	impcom 445	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))
129	128	3adant1 1072	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))
130		raleq 3115	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑧 → (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
131		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑧 → (𝑎‘𝑡) = (𝑎‘𝑧))
132		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑧 → (𝑐‘𝑡) = (𝑐‘𝑧))
133	131, 132	breq12d 4596	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑧 → ((𝑎‘𝑡)𝑅(𝑐‘𝑡) ↔ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
134	130, 133	anbi12d 743	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑧 → ((∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧))))
135	134	rspcev 3282	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ On ∧ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
136	104, 117, 129, 135	syl12anc 1316	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
137	136	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
138	137	3exp 1256	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ∈ 𝑤 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
139	2	orderseqlem 30993	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ 𝐹 → (𝑎‘𝑧) ∈ (𝐴 ∪ {∅}))
140	139	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (𝑎‘𝑧) ∈ (𝐴 ∪ {∅}))
141	2	orderseqlem 30993	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ∈ 𝐹 → (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}))
142	141	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}))
143	2	orderseqlem 30993	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ 𝐹 → (𝑐‘𝑧) ∈ (𝐴 ∪ {∅}))
144	143	ad2antll 761	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (𝑐‘𝑧) ∈ (𝐴 ∪ {∅}))
145	140, 142, 144	3jca 1235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ((𝑎‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐‘𝑧) ∈ (𝐴 ∪ {∅})))
146		potr 4971	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Po (𝐴 ∪ {∅}) ∧ ((𝑎‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐‘𝑧) ∈ (𝐴 ∪ {∅}))) → (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
147	1, 145, 146	sylancr 694	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
148	147	impcom 445	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹))) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))
149	113, 148	anim12i 588	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))) → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
150	149	anassrs 678	. . . . . . . . . . . . . . . . . 18 ⊢ (((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹))) → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
151	150, 135	sylan2 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ On ∧ ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
152	151	exp32 629	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ On → ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))))
153		raleq 3115	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑤 → (∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)))
154	153	anbi2d 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦))))
155	110, 154	syl5bb 271	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑤 → (∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦))))
156		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑤 → (𝑏‘𝑧) = (𝑏‘𝑤))
157		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑤 → (𝑐‘𝑧) = (𝑐‘𝑤))
158	156, 157	breq12d 4596	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → ((𝑏‘𝑧)𝑅(𝑐‘𝑧) ↔ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))
159	158	anbi2d 736	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑤 → (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) ↔ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
160	155, 159	anbi12d 743	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑤 → ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) ↔ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))))
161	160	imbi1d 330	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑤 → (((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))) ↔ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
162	152, 161	syl5ibcom 234	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ On → (𝑧 = 𝑤 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
163	162	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 = 𝑤 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
164		simp1r 1079	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑤 ∈ On)
165		onelss 5683	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ On → (𝑤 ∈ 𝑧 → 𝑤 ⊆ 𝑧))
166	165	imp 444	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ 𝑧) → 𝑤 ⊆ 𝑧)
167	166	adantlr 747	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧) → 𝑤 ⊆ 𝑧)
168		ssralv 3629	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ⊆ 𝑧 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦)))
169	168	anim1d 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ⊆ 𝑧 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦))))
170		r19.26 3046	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ 𝑤 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)))
171	112	ralimi 2936	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ 𝑤 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦))
172	170, 171	sylbir 224	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦))
173	169, 172	syl6 34	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ⊆ 𝑧 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
174	173	adantrd 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ⊆ 𝑧 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
175	167, 174	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
176	175	3impia 1253	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦))
177		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑤 → (𝑎‘𝑦) = (𝑎‘𝑤))
178		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑤 → (𝑏‘𝑦) = (𝑏‘𝑤))
179	177, 178	eqeq12d 2625	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑤 → ((𝑎‘𝑦) = (𝑏‘𝑦) ↔ (𝑎‘𝑤) = (𝑏‘𝑤)))
180	179	rspcv 3278	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ 𝑧 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑤) = (𝑏‘𝑤)))
181		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎‘𝑤) = (𝑏‘𝑤) → ((𝑎‘𝑤)𝑅(𝑐‘𝑤) ↔ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))
182	181	biimprd 237	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎‘𝑤) = (𝑏‘𝑤) → ((𝑏‘𝑤)𝑅(𝑐‘𝑤) → (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
183	180, 182	syl6 34	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ 𝑧 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → ((𝑏‘𝑤)𝑅(𝑐‘𝑤) → (𝑎‘𝑤)𝑅(𝑐‘𝑤))))
184	183	com3l 87	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → ((𝑏‘𝑤)𝑅(𝑐‘𝑤) → (𝑤 ∈ 𝑧 → (𝑎‘𝑤)𝑅(𝑐‘𝑤))))
185	184	imp 444	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)) → (𝑤 ∈ 𝑧 → (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
186	185	ad2ant2rl 781	. . . . . . . . . . . . . . . . . . 19 ⊢ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (𝑤 ∈ 𝑧 → (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
187	186	impcom 445	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑤)𝑅(𝑐‘𝑤))
188	187	3adant1 1072	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑤)𝑅(𝑐‘𝑤))
189		raleq 3115	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑤 → (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
190		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑤 → (𝑎‘𝑡) = (𝑎‘𝑤))
191		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑤 → (𝑐‘𝑡) = (𝑐‘𝑤))
192	190, 191	breq12d 4596	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑤 → ((𝑎‘𝑡)𝑅(𝑐‘𝑡) ↔ (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
193	189, 192	anbi12d 743	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑤 → ((∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)) ↔ (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑤)𝑅(𝑐‘𝑤))))
194	193	rspcev 3282	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ On ∧ (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑤)𝑅(𝑐‘𝑤))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
195	164, 176, 188, 194	syl12anc 1316	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
196	195	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
197	196	3exp 1256	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑤 ∈ 𝑧 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
198	138, 163, 197	3jaod 1384	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → ((𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
199	103, 198	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))))
200	199	rexlimivv 3018	. . . . . . . . . . 11 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
201	99, 200	sylbir 224	. . . . . . . . . 10 ⊢ ((∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
202	201	impcom 445	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
203	94, 95, 202	jca31 555	. . . . . . . 8 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
204	203	an4s 865	. . . . . . 7 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))) ∧ ((𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
205	64, 93, 204	syl2anb 495	. . . . . 6 ⊢ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
206		raleq 3115	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦)))
207		fveq2 6103	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → (𝑓‘𝑥) = (𝑓‘𝑡))
208		fveq2 6103	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → (𝑔‘𝑥) = (𝑔‘𝑡))
209	207, 208	breq12d 4596	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑓‘𝑡)𝑅(𝑔‘𝑡)))
210	206, 209	anbi12d 743	. . . . . . . . . 10 ⊢ (𝑥 = 𝑡 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡))))
211	210	cbvrexv 3148	. . . . . . . . 9 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡)))
212	20	ralbidv 2969	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦)))
213		fveq1 6102	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑡) = (𝑎‘𝑡))
214	213	breq1d 4593	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑡)𝑅(𝑔‘𝑡) ↔ (𝑎‘𝑡)𝑅(𝑔‘𝑡)))
215	212, 214	anbi12d 743	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡)) ↔ (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))))
216	215	rexbidv 3034	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → (∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))))
217	211, 216	syl5bb 271	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))))
218	18, 217	anbi12d 743	. . . . . . 7 ⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡)))))
219	83	anbi2d 736	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))
220	85	eqeq2d 2620	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑐‘𝑦)))
221	220	ralbidv 2969	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦)))
222		fveq1 6102	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → (𝑔‘𝑡) = (𝑐‘𝑡))
223	222	breq2d 4595	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → ((𝑎‘𝑡)𝑅(𝑔‘𝑡) ↔ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
224	221, 223	anbi12d 743	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → ((∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡)) ↔ (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
225	224	rexbidv 3034	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
226	219, 225	anbi12d 743	. . . . . . 7 ⊢ (𝑔 = 𝑐 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))))
227	16, 65, 218, 226, 37	brab 4923	. . . . . 6 ⊢ (𝑎𝑆𝑐 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
228	205, 227	sylibr 223	. . . . 5 ⊢ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)
229	39, 228	pm3.2i 470	. . . 4 ⊢ (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐))
230	229	a1i 11	. . 3 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) → (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
231	230	rgen3 2959	. 2 ⊢ ∀𝑎 ∈ 𝐹 ∀𝑏 ∈ 𝐹 ∀𝑐 ∈ 𝐹 (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐))
232		df-po 4959	. 2 ⊢ (𝑆 Po 𝐹 ↔ ∀𝑎 ∈ 𝐹 ∀𝑏 ∈ 𝐹 ∀𝑐 ∈ 𝐹 (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
233	231, 232	mpbir 220	1 ⊢ 𝑆 Po 𝐹

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∨ w3o 1030   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  {cab 2596  ∀wral 2896  ∃wrex 2897   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874  {csn 4125   class class class wbr 4583  {copab 4642   Po wpo 4957  Ord word 5639  Oncon0 5640  ⟶wf 5800  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-tr 4681  df-eprel 4949  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-ord 5643  df-on 5644  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812

This theorem is referenced by:  soseq  30995