Theorem poseq 8159

Description: A partial ordering of ordinal sequences. (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 6680	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑏 → (𝑓:𝑥⟶𝐴 ↔ 𝑓:𝑏⟶𝐴))
4	3	cbvrexvw 3242	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥 ∈ On 𝑓:𝑥⟶𝐴 ↔ ∃𝑏 ∈ On 𝑓:𝑏⟶𝐴)
5	4	abbii 2828	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏⟶𝐴}
6	2, 5	eqtri 2784	. . . . . . . . . . . . 13 ⊢ 𝐹 = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏⟶𝐴}
7	6	orderseqlem 8158	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝐹 → (𝑎‘𝑥) ∈ (𝐴 ∪ {∅}))
8		poirr 5571	. . . . . . . . . . . 12 ⊢ ((𝑅 Po (𝐴 ∪ {∅}) ∧ (𝑎‘𝑥) ∈ (𝐴 ∪ {∅})) → ¬ (𝑎‘𝑥)𝑅(𝑎‘𝑥))
9	1, 7, 8	sylancr 599	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝐹 → ¬ (𝑎‘𝑥)𝑅(𝑎‘𝑥))
10	9	intnand 494	. . . . . . . . . 10 ⊢ (𝑎 ∈ 𝐹 → ¬ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
11	10	adantr 486	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑥 ∈ On) → ¬ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
12	11	nrexdv 3158	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐹 → ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
13	12	adantr 486	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
14		imnan 405	. . . . . . 7 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))) ↔ ¬ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
15	13, 14	mpbi 233	. . . . . 6 ⊢ ¬ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
16		vex 3455	. . . . . . 7 ⊢ 𝑎 ∈ V
17		eleq1w 2844	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → (𝑓 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹))
18	17	anbi1d 643	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹)))
19		fveq1 6876	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑦) = (𝑎‘𝑦))
20	19	eqeq1d 2763	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑔‘𝑦)))
21	20	ralbidv 3186	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦)))
22		fveq1 6876	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑥) = (𝑎‘𝑥))
23	22	breq1d 5113	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))
24	21, 23	anbi12d 644	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))))
25	24	rexbidv 3187	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))))
26	18, 25	anbi12d 644	. . . . . . 7 ⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))))
27		eleq1w 2844	. . . . . . . . 9 ⊢ (𝑔 = 𝑎 → (𝑔 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹))
28	27	anbi2d 642	. . . . . . . 8 ⊢ (𝑔 = 𝑎 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹)))
29		fveq1 6876	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑦) = (𝑎‘𝑦))
30	29	eqeq2d 2772	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑎 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑎‘𝑦)))
31	30	ralbidv 3186	. . . . . . . . . 10 ⊢ (𝑔 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦)))
32		fveq1 6876	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑥) = (𝑎‘𝑥))
33	32	breq2d 5115	. . . . . . . . . 10 ⊢ (𝑔 = 𝑎 → ((𝑎‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
34	31, 33	anbi12d 644	. . . . . . . . 9 ⊢ (𝑔 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
35	34	rexbidv 3187	. . . . . . . 8 ⊢ (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
36	28, 35	anbi12d 644	. . . . . . 7 ⊢ (𝑔 = 𝑎 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))))
37		poseq.3	. . . . . . 7 ⊢ 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))}
38	16, 16, 26, 36, 37	brab 5518	. . . . . 6 ⊢ (𝑎𝑆𝑎 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
39	15, 38	mtbir 326	. . . . 5 ⊢ ¬ 𝑎𝑆𝑎
40		vex 3455	. . . . . . . 8 ⊢ 𝑏 ∈ V
41		raleq 3317	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦)))
42		fveq2 6877	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑓‘𝑥) = (𝑓‘𝑧))
43		fveq2 6877	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑔‘𝑥) = (𝑔‘𝑧))
44	42, 43	breq12d 5116	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑓‘𝑧)𝑅(𝑔‘𝑧)))
45	41, 44	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧))))
46	45	cbvrexvw 3242	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧)))
47	20	ralbidv 3186	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦)))
48		fveq1 6876	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑧) = (𝑎‘𝑧))
49	48	breq1d 5113	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑧)𝑅(𝑔‘𝑧) ↔ (𝑎‘𝑧)𝑅(𝑔‘𝑧)))
50	47, 49	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))))
51	50	rexbidv 3187	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))))
52	46, 51	bitrid 286	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))))
53	18, 52	anbi12d 644	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧)))))
54		eleq1w 2844	. . . . . . . . . 10 ⊢ (𝑔 = 𝑏 → (𝑔 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹))
55	54	anbi2d 642	. . . . . . . . 9 ⊢ (𝑔 = 𝑏 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹)))
56		fveq1 6876	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑦) = (𝑏‘𝑦))
57	56	eqeq2d 2772	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑏 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑏‘𝑦)))
58	57	ralbidv 3186	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑏 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦)))
59		fveq1 6876	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑧) = (𝑏‘𝑧))
60	59	breq2d 5115	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑏 → ((𝑎‘𝑧)𝑅(𝑔‘𝑧) ↔ (𝑎‘𝑧)𝑅(𝑏‘𝑧)))
61	58, 60	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑔 = 𝑏 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))))
62	61	rexbidv 3187	. . . . . . . . 9 ⊢ (𝑔 = 𝑏 → (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))))
63	55, 62	anbi12d 644	. . . . . . . 8 ⊢ (𝑔 = 𝑏 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)))))
64	16, 40, 53, 63, 37	brab 5518	. . . . . . 7 ⊢ (𝑎𝑆𝑏 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))))
65		vex 3455	. . . . . . . 8 ⊢ 𝑐 ∈ V
66		eleq1w 2844	. . . . . . . . . 10 ⊢ (𝑓 = 𝑏 → (𝑓 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹))
67	66	anbi1d 643	. . . . . . . . 9 ⊢ (𝑓 = 𝑏 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹)))
68		raleq 3317	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦)))
69		fveq2 6877	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → (𝑓‘𝑥) = (𝑓‘𝑤))
70		fveq2 6877	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → (𝑔‘𝑥) = (𝑔‘𝑤))
71	69, 70	breq12d 5116	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑓‘𝑤)𝑅(𝑔‘𝑤)))
72	68, 71	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤))))
73	72	cbvrexvw 3242	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤)))
74		fveq1 6876	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑦) = (𝑏‘𝑦))
75	74	eqeq1d 2763	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑔‘𝑦)))
76	75	ralbidv 3186	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦)))
77		fveq1 6876	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑤) = (𝑏‘𝑤))
78	77	breq1d 5113	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑤)𝑅(𝑔‘𝑤) ↔ (𝑏‘𝑤)𝑅(𝑔‘𝑤)))
79	76, 78	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑏 → ((∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤)) ↔ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))))
80	79	rexbidv 3187	. . . . . . . . . 10 ⊢ (𝑓 = 𝑏 → (∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))))
81	73, 80	bitrid 286	. . . . . . . . 9 ⊢ (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))))
82	67, 81	anbi12d 644	. . . . . . . 8 ⊢ (𝑓 = 𝑏 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤)))))
83		eleq1w 2844	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → (𝑔 ∈ 𝐹 ↔ 𝑐 ∈ 𝐹))
84	83	anbi2d 642	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))
85		fveq1 6876	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑐 → (𝑔‘𝑦) = (𝑐‘𝑦))
86	85	eqeq2d 2772	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑐 → ((𝑏‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑐‘𝑦)))
87	86	ralbidv 3186	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)))
88		fveq1 6876	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑐 → (𝑔‘𝑤) = (𝑐‘𝑤))
89	88	breq2d 5115	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → ((𝑏‘𝑤)𝑅(𝑔‘𝑤) ↔ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))
90	87, 89	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → ((∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤)) ↔ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
91	90	rexbidv 3187	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → (∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
92	84, 91	anbi12d 644	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))))
93	40, 65, 82, 92, 37	brab 5518	. . . . . . 7 ⊢ (𝑏𝑆𝑐 ↔ ((𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
94		simplll 787	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑎 ∈ 𝐹)
95		simplrr 790	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑐 ∈ 𝐹)
96		an4 669	. . . . . . . . . . . . 13 ⊢ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
97	96	2rexbii 3139	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ ∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
98		reeanv 3235	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
99	97, 98	bitri 278	. . . . . . . . . . 11 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
100		eloni 6365	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ On → Ord 𝑧)
101		eloni 6365	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ On → Ord 𝑤)
102		ordtri3or 6388	. . . . . . . . . . . . . 14 ⊢ ((Ord 𝑧 ∧ Ord 𝑤) → (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))
103	100, 101, 102	syl2an 608	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))
104		simp1l 1216	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑧 ∈ On)
105		onelss 6398	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ On → (𝑧 ∈ 𝑤 → 𝑧 ⊆ 𝑤))
106	105	imp 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤 ∈ On ∧ 𝑧 ∈ 𝑤) → 𝑧 ⊆ 𝑤)
107	106	adantll 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤) → 𝑧 ⊆ 𝑤)
108		ssralv 4000	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ⊆ 𝑤 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦)))
109	108	anim2d 624	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ⊆ 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦))))
110		r19.26 3123	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦)))
111	109, 110	imbitrrdi 255	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ⊆ 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦))))
112		eqtr 2781	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) → (𝑎‘𝑦) = (𝑐‘𝑦))
113	112	ralimi 3100	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦))
114	111, 113	syl6 36	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ⊆ 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
115	107, 114	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤) → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
116	115	adantrd 497	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
117	116	3impia 1135	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦))
118		fveq2 6877	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑧 → (𝑏‘𝑦) = (𝑏‘𝑧))
119		fveq2 6877	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑧 → (𝑐‘𝑦) = (𝑐‘𝑧))
120	118, 119	eqeq12d 2777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑧 → ((𝑏‘𝑦) = (𝑐‘𝑦) ↔ (𝑏‘𝑧) = (𝑐‘𝑧)))
121	120	rspcv 3573	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ 𝑤 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → (𝑏‘𝑧) = (𝑐‘𝑧)))
122		breq2 5107	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏‘𝑧) = (𝑐‘𝑧) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ↔ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
123	122	biimpd 232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏‘𝑧) = (𝑐‘𝑧) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
124	121, 123	syl6 36	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ 𝑤 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))))
125	124	com3l 90	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) → (𝑧 ∈ 𝑤 → (𝑎‘𝑧)𝑅(𝑐‘𝑧))))
126	125	imp 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) → (𝑧 ∈ 𝑤 → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
127	126	ad2ant2lr 761	. . . . . . . . . . . . . . . . . . 19 ⊢ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (𝑧 ∈ 𝑤 → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
128	127	impcom 413	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))
129	128	3adant1 1148	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))
130		raleq 3317	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑧 → (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
131		fveq2 6877	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑧 → (𝑎‘𝑡) = (𝑎‘𝑧))
132		fveq2 6877	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑧 → (𝑐‘𝑡) = (𝑐‘𝑧))
133	131, 132	breq12d 5116	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑧 → ((𝑎‘𝑡)𝑅(𝑐‘𝑡) ↔ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
134	130, 133	anbi12d 644	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑧 → ((∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧))))
135	134	rspcev 3577	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ On ∧ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
136	104, 117, 129, 135	syl12anc 850	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
137	136	a1d 26	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
138	137	3exp 1137	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ∈ 𝑤 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
139	2	orderseqlem 8158	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ 𝐹 → (𝑎‘𝑧) ∈ (𝐴 ∪ {∅}))
140	139	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (𝑎‘𝑧) ∈ (𝐴 ∪ {∅}))
141	2	orderseqlem 8158	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ∈ 𝐹 → (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}))
142	141	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}))
143	2	orderseqlem 8158	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ 𝐹 → (𝑐‘𝑧) ∈ (𝐴 ∪ {∅}))
144	143	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (𝑐‘𝑧) ∈ (𝐴 ∪ {∅}))
145	140, 142, 144	3jca 1146	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ((𝑎‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐‘𝑧) ∈ (𝐴 ∪ {∅})))
146		potr 5572	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Po (𝐴 ∪ {∅}) ∧ ((𝑎‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐‘𝑧) ∈ (𝐴 ∪ {∅}))) → (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
147	1, 145, 146	sylancr 599	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
148	147	impcom 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹))) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))
149	113, 148	anim12i 625	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))) → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
150	149	anassrs 473	. . . . . . . . . . . . . . . . . 18 ⊢ (((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹))) → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
151	150, 135	sylan2 605	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ On ∧ ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
152	151	exp32 426	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ On → ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))))
153		raleq 3317	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑤 → (∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)))
154	153	anbi2d 642	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦))))
155	110, 154	bitrid 286	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑤 → (∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦))))
156		fveq2 6877	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑤 → (𝑏‘𝑧) = (𝑏‘𝑤))
157		fveq2 6877	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑤 → (𝑐‘𝑧) = (𝑐‘𝑤))
158	156, 157	breq12d 5116	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → ((𝑏‘𝑧)𝑅(𝑐‘𝑧) ↔ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))
159	158	anbi2d 642	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑤 → (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) ↔ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
160	155, 159	anbi12d 644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑤 → ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) ↔ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))))
161	160	imbi1d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑤 → (((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))) ↔ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
162	152, 161	syl5ibcom 248	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ On → (𝑧 = 𝑤 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
163	162	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 = 𝑤 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
164		simp1r 1217	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑤 ∈ On)
165		onelss 6398	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ On → (𝑤 ∈ 𝑧 → 𝑤 ⊆ 𝑧))
166	165	imp 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ 𝑧) → 𝑤 ⊆ 𝑧)
167	166	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧) → 𝑤 ⊆ 𝑧)
168		ssralv 4000	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ⊆ 𝑧 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦)))
169	168	anim1d 623	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ⊆ 𝑧 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦))))
170		r19.26 3123	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ 𝑤 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)))
171	112	ralimi 3100	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ 𝑤 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦))
172	170, 171	sylbir 238	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦))
173	169, 172	syl6 36	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ⊆ 𝑧 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
174	173	adantrd 497	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ⊆ 𝑧 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
175	167, 174	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
176	175	3impia 1135	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦))
177		fveq2 6877	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑤 → (𝑎‘𝑦) = (𝑎‘𝑤))
178		fveq2 6877	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑤 → (𝑏‘𝑦) = (𝑏‘𝑤))
179	177, 178	eqeq12d 2777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑤 → ((𝑎‘𝑦) = (𝑏‘𝑦) ↔ (𝑎‘𝑤) = (𝑏‘𝑤)))
180	179	rspcv 3573	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ 𝑧 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑤) = (𝑏‘𝑤)))
181		breq1 5106	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎‘𝑤) = (𝑏‘𝑤) → ((𝑎‘𝑤)𝑅(𝑐‘𝑤) ↔ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))
182	181	biimprd 251	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎‘𝑤) = (𝑏‘𝑤) → ((𝑏‘𝑤)𝑅(𝑐‘𝑤) → (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
183	180, 182	syl6 36	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ 𝑧 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → ((𝑏‘𝑤)𝑅(𝑐‘𝑤) → (𝑎‘𝑤)𝑅(𝑐‘𝑤))))
184	183	com3l 90	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → ((𝑏‘𝑤)𝑅(𝑐‘𝑤) → (𝑤 ∈ 𝑧 → (𝑎‘𝑤)𝑅(𝑐‘𝑤))))
185	184	imp 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)) → (𝑤 ∈ 𝑧 → (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
186	185	ad2ant2rl 762	. . . . . . . . . . . . . . . . . . 19 ⊢ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (𝑤 ∈ 𝑧 → (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
187	186	impcom 413	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑤)𝑅(𝑐‘𝑤))
188	187	3adant1 1148	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑤)𝑅(𝑐‘𝑤))
189		raleq 3317	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑤 → (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
190		fveq2 6877	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑤 → (𝑎‘𝑡) = (𝑎‘𝑤))
191		fveq2 6877	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑤 → (𝑐‘𝑡) = (𝑐‘𝑤))
192	190, 191	breq12d 5116	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑤 → ((𝑎‘𝑡)𝑅(𝑐‘𝑡) ↔ (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
193	189, 192	anbi12d 644	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑤 → ((∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)) ↔ (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑤)𝑅(𝑐‘𝑤))))
194	193	rspcev 3577	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ On ∧ (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑤)𝑅(𝑐‘𝑤))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
195	164, 176, 188, 194	syl12anc 850	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
196	195	a1d 26	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
197	196	3exp 1137	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑤 ∈ 𝑧 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
198	138, 163, 197	3jaod 1456	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → ((𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
199	103, 198	mpd 16	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))))
200	199	rexlimivv 3205	. . . . . . . . . . 11 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
201	99, 200	sylbir 238	. . . . . . . . . 10 ⊢ ((∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
202	201	impcom 413	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
203	94, 95, 202	jca31 524	. . . . . . . 8 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
204	203	an4s 673	. . . . . . 7 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))) ∧ ((𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
205	64, 93, 204	syl2anb 610	. . . . . 6 ⊢ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
206		raleq 3317	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦)))
207		fveq2 6877	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → (𝑓‘𝑥) = (𝑓‘𝑡))
208		fveq2 6877	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → (𝑔‘𝑥) = (𝑔‘𝑡))
209	207, 208	breq12d 5116	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑓‘𝑡)𝑅(𝑔‘𝑡)))
210	206, 209	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑥 = 𝑡 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡))))
211	210	cbvrexvw 3242	. . . . . . . . 9 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡)))
212	20	ralbidv 3186	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦)))
213		fveq1 6876	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑡) = (𝑎‘𝑡))
214	213	breq1d 5113	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑡)𝑅(𝑔‘𝑡) ↔ (𝑎‘𝑡)𝑅(𝑔‘𝑡)))
215	212, 214	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡)) ↔ (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))))
216	215	rexbidv 3187	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → (∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))))
217	211, 216	bitrid 286	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))))
218	18, 217	anbi12d 644	. . . . . . 7 ⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡)))))
219	83	anbi2d 642	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))
220	85	eqeq2d 2772	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑐‘𝑦)))
221	220	ralbidv 3186	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦)))
222		fveq1 6876	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → (𝑔‘𝑡) = (𝑐‘𝑡))
223	222	breq2d 5115	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → ((𝑎‘𝑡)𝑅(𝑔‘𝑡) ↔ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
224	221, 223	anbi12d 644	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → ((∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡)) ↔ (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
225	224	rexbidv 3187	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
226	219, 225	anbi12d 644	. . . . . . 7 ⊢ (𝑔 = 𝑐 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))))
227	16, 65, 218, 226, 37	brab 5518	. . . . . 6 ⊢ (𝑎𝑆𝑐 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
228	205, 227	sylibr 237	. . . . 5 ⊢ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)
229	39, 228	pm3.2i 476	. . . 4 ⊢ (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐))
230	229	a1i 11	. . 3 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) → (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
231	230	rgen3 3208	. 2 ⊢ ∀𝑎 ∈ 𝐹 ∀𝑏 ∈ 𝐹 ∀𝑐 ∈ 𝐹 (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐))
232		df-po 5559	. 2 ⊢ (𝑆 Po 𝐹 ↔ ∀𝑎 ∈ 𝐹 ∀𝑏 ∈ 𝐹 ∀𝑐 ∈ 𝐹 (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
233	231, 232	mpbir 234	1 ⊢ 𝑆 Po 𝐹

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ w3o 1102   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  {cab 2739  ∀wral 3077  ∃wrex 3087   ∪ cun 3897   ⊆ wss 3899  ∅c0 4279  {csn 4584   class class class wbr 5103  {copab 5167   Po wpo 5557  Ord word 6354  Oncon0 6355  ⟶wf 6527  ‘cfv 6531

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-ord 6358  df-on 6359  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539

This theorem is used by:  soseq  8160