Theorem poseq 33090

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 6491	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑏 → (𝑓:𝑥⟶𝐴 ↔ 𝑓:𝑏⟶𝐴))
4	3	cbvrexvw 3451	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥 ∈ On 𝑓:𝑥⟶𝐴 ↔ ∃𝑏 ∈ On 𝑓:𝑏⟶𝐴)
5	4	abbii 2886	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏⟶𝐴}
6	2, 5	eqtri 2844	. . . . . . . . . . . . 13 ⊢ 𝐹 = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏⟶𝐴}
7	6	orderseqlem 33089	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝐹 → (𝑎‘𝑥) ∈ (𝐴 ∪ {∅}))
8		poirr 5480	. . . . . . . . . . . 12 ⊢ ((𝑅 Po (𝐴 ∪ {∅}) ∧ (𝑎‘𝑥) ∈ (𝐴 ∪ {∅})) → ¬ (𝑎‘𝑥)𝑅(𝑎‘𝑥))
9	1, 7, 8	sylancr 589	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝐹 → ¬ (𝑎‘𝑥)𝑅(𝑎‘𝑥))
10	9	intnand 491	. . . . . . . . . 10 ⊢ (𝑎 ∈ 𝐹 → ¬ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
11	10	adantr 483	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑥 ∈ On) → ¬ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
12	11	nrexdv 3270	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐹 → ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
13	12	adantr 483	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
14		imnan 402	. . . . . . 7 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))) ↔ ¬ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
15	13, 14	mpbi 232	. . . . . 6 ⊢ ¬ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
16		vex 3498	. . . . . . 7 ⊢ 𝑎 ∈ V
17		eleq1w 2895	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → (𝑓 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹))
18	17	anbi1d 631	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹)))
19		fveq1 6664	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑦) = (𝑎‘𝑦))
20	19	eqeq1d 2823	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑔‘𝑦)))
21	20	ralbidv 3197	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦)))
22		fveq1 6664	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑥) = (𝑎‘𝑥))
23	22	breq1d 5069	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))
24	21, 23	anbi12d 632	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))))
25	24	rexbidv 3297	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))))
26	18, 25	anbi12d 632	. . . . . . 7 ⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))))
27		eleq1w 2895	. . . . . . . . 9 ⊢ (𝑔 = 𝑎 → (𝑔 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹))
28	27	anbi2d 630	. . . . . . . 8 ⊢ (𝑔 = 𝑎 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹)))
29		fveq1 6664	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑦) = (𝑎‘𝑦))
30	29	eqeq2d 2832	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑎 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑎‘𝑦)))
31	30	ralbidv 3197	. . . . . . . . . 10 ⊢ (𝑔 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦)))
32		fveq1 6664	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑥) = (𝑎‘𝑥))
33	32	breq2d 5071	. . . . . . . . . 10 ⊢ (𝑔 = 𝑎 → ((𝑎‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
34	31, 33	anbi12d 632	. . . . . . . . 9 ⊢ (𝑔 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
35	34	rexbidv 3297	. . . . . . . 8 ⊢ (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
36	28, 35	anbi12d 632	. . . . . . 7 ⊢ (𝑔 = 𝑎 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))))
37		poseq.3	. . . . . . 7 ⊢ 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))}
38	16, 16, 26, 36, 37	brab 5423	. . . . . 6 ⊢ (𝑎𝑆𝑎 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
39	15, 38	mtbir 325	. . . . 5 ⊢ ¬ 𝑎𝑆𝑎
40		vex 3498	. . . . . . . 8 ⊢ 𝑏 ∈ V
41		raleq 3406	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦)))
42		fveq2 6665	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑓‘𝑥) = (𝑓‘𝑧))
43		fveq2 6665	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑔‘𝑥) = (𝑔‘𝑧))
44	42, 43	breq12d 5072	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑓‘𝑧)𝑅(𝑔‘𝑧)))
45	41, 44	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧))))
46	45	cbvrexvw 3451	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧)))
47	20	ralbidv 3197	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦)))
48		fveq1 6664	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑧) = (𝑎‘𝑧))
49	48	breq1d 5069	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑧)𝑅(𝑔‘𝑧) ↔ (𝑎‘𝑧)𝑅(𝑔‘𝑧)))
50	47, 49	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))))
51	50	rexbidv 3297	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))))
52	46, 51	syl5bb 285	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))))
53	18, 52	anbi12d 632	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧)))))
54		eleq1w 2895	. . . . . . . . . 10 ⊢ (𝑔 = 𝑏 → (𝑔 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹))
55	54	anbi2d 630	. . . . . . . . 9 ⊢ (𝑔 = 𝑏 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹)))
56		fveq1 6664	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑦) = (𝑏‘𝑦))
57	56	eqeq2d 2832	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑏 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑏‘𝑦)))
58	57	ralbidv 3197	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑏 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦)))
59		fveq1 6664	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑧) = (𝑏‘𝑧))
60	59	breq2d 5071	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑏 → ((𝑎‘𝑧)𝑅(𝑔‘𝑧) ↔ (𝑎‘𝑧)𝑅(𝑏‘𝑧)))
61	58, 60	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑔 = 𝑏 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))))
62	61	rexbidv 3297	. . . . . . . . 9 ⊢ (𝑔 = 𝑏 → (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))))
63	55, 62	anbi12d 632	. . . . . . . 8 ⊢ (𝑔 = 𝑏 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)))))
64	16, 40, 53, 63, 37	brab 5423	. . . . . . 7 ⊢ (𝑎𝑆𝑏 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))))
65		vex 3498	. . . . . . . 8 ⊢ 𝑐 ∈ V
66		eleq1w 2895	. . . . . . . . . 10 ⊢ (𝑓 = 𝑏 → (𝑓 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹))
67	66	anbi1d 631	. . . . . . . . 9 ⊢ (𝑓 = 𝑏 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹)))
68		raleq 3406	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦)))
69		fveq2 6665	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → (𝑓‘𝑥) = (𝑓‘𝑤))
70		fveq2 6665	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → (𝑔‘𝑥) = (𝑔‘𝑤))
71	69, 70	breq12d 5072	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑓‘𝑤)𝑅(𝑔‘𝑤)))
72	68, 71	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤))))
73	72	cbvrexvw 3451	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤)))
74		fveq1 6664	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑦) = (𝑏‘𝑦))
75	74	eqeq1d 2823	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑔‘𝑦)))
76	75	ralbidv 3197	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦)))
77		fveq1 6664	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑤) = (𝑏‘𝑤))
78	77	breq1d 5069	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑤)𝑅(𝑔‘𝑤) ↔ (𝑏‘𝑤)𝑅(𝑔‘𝑤)))
79	76, 78	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑏 → ((∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤)) ↔ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))))
80	79	rexbidv 3297	. . . . . . . . . 10 ⊢ (𝑓 = 𝑏 → (∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))))
81	73, 80	syl5bb 285	. . . . . . . . 9 ⊢ (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))))
82	67, 81	anbi12d 632	. . . . . . . 8 ⊢ (𝑓 = 𝑏 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤)))))
83		eleq1w 2895	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → (𝑔 ∈ 𝐹 ↔ 𝑐 ∈ 𝐹))
84	83	anbi2d 630	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))
85		fveq1 6664	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑐 → (𝑔‘𝑦) = (𝑐‘𝑦))
86	85	eqeq2d 2832	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑐 → ((𝑏‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑐‘𝑦)))
87	86	ralbidv 3197	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)))
88		fveq1 6664	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑐 → (𝑔‘𝑤) = (𝑐‘𝑤))
89	88	breq2d 5071	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → ((𝑏‘𝑤)𝑅(𝑔‘𝑤) ↔ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))
90	87, 89	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → ((∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤)) ↔ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
91	90	rexbidv 3297	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → (∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
92	84, 91	anbi12d 632	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))))
93	40, 65, 82, 92, 37	brab 5423	. . . . . . 7 ⊢ (𝑏𝑆𝑐 ↔ ((𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
94		simplll 773	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑎 ∈ 𝐹)
95		simplrr 776	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑐 ∈ 𝐹)
96		an4 654	. . . . . . . . . . . . 13 ⊢ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
97	96	2rexbii 3248	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ ∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
98		reeanv 3368	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
99	97, 98	bitri 277	. . . . . . . . . . 11 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
100		eloni 6196	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ On → Ord 𝑧)
101		eloni 6196	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ On → Ord 𝑤)
102		ordtri3or 6218	. . . . . . . . . . . . . 14 ⊢ ((Ord 𝑧 ∧ Ord 𝑤) → (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))
103	100, 101, 102	syl2an 597	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))
104		simp1l 1193	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑧 ∈ On)
105		onelss 6228	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ On → (𝑧 ∈ 𝑤 → 𝑧 ⊆ 𝑤))
106	105	imp 409	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤 ∈ On ∧ 𝑧 ∈ 𝑤) → 𝑧 ⊆ 𝑤)
107	106	adantll 712	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤) → 𝑧 ⊆ 𝑤)
108		ssralv 4033	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ⊆ 𝑤 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦)))
109	108	anim2d 613	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ⊆ 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦))))
110		r19.26 3170	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦)))
111	109, 110	syl6ibr 254	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ⊆ 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦))))
112		eqtr 2841	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) → (𝑎‘𝑦) = (𝑐‘𝑦))
113	112	ralimi 3160	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦))
114	111, 113	syl6 35	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ⊆ 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
115	107, 114	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤) → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
116	115	adantrd 494	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
117	116	3impia 1113	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦))
118		fveq2 6665	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑧 → (𝑏‘𝑦) = (𝑏‘𝑧))
119		fveq2 6665	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑧 → (𝑐‘𝑦) = (𝑐‘𝑧))
120	118, 119	eqeq12d 2837	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑧 → ((𝑏‘𝑦) = (𝑐‘𝑦) ↔ (𝑏‘𝑧) = (𝑐‘𝑧)))
121	120	rspcv 3618	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ 𝑤 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → (𝑏‘𝑧) = (𝑐‘𝑧)))
122		breq2 5063	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏‘𝑧) = (𝑐‘𝑧) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ↔ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
123	122	biimpd 231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏‘𝑧) = (𝑐‘𝑧) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
124	121, 123	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ 𝑤 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))))
125	124	com3l 89	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) → (𝑧 ∈ 𝑤 → (𝑎‘𝑧)𝑅(𝑐‘𝑧))))
126	125	imp 409	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) → (𝑧 ∈ 𝑤 → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
127	126	ad2ant2lr 746	. . . . . . . . . . . . . . . . . . 19 ⊢ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (𝑧 ∈ 𝑤 → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
128	127	impcom 410	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))
129	128	3adant1 1126	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))
130		raleq 3406	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑧 → (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
131		fveq2 6665	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑧 → (𝑎‘𝑡) = (𝑎‘𝑧))
132		fveq2 6665	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑧 → (𝑐‘𝑡) = (𝑐‘𝑧))
133	131, 132	breq12d 5072	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑧 → ((𝑎‘𝑡)𝑅(𝑐‘𝑡) ↔ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
134	130, 133	anbi12d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑧 → ((∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧))))
135	134	rspcev 3623	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ On ∧ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
136	104, 117, 129, 135	syl12anc 834	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
137	136	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
138	137	3exp 1115	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ∈ 𝑤 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
139	2	orderseqlem 33089	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ 𝐹 → (𝑎‘𝑧) ∈ (𝐴 ∪ {∅}))
140	139	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (𝑎‘𝑧) ∈ (𝐴 ∪ {∅}))
141	2	orderseqlem 33089	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ∈ 𝐹 → (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}))
142	141	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}))
143	2	orderseqlem 33089	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ 𝐹 → (𝑐‘𝑧) ∈ (𝐴 ∪ {∅}))
144	143	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (𝑐‘𝑧) ∈ (𝐴 ∪ {∅}))
145	140, 142, 144	3jca 1124	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ((𝑎‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐‘𝑧) ∈ (𝐴 ∪ {∅})))
146		potr 5481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Po (𝐴 ∪ {∅}) ∧ ((𝑎‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐‘𝑧) ∈ (𝐴 ∪ {∅}))) → (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
147	1, 145, 146	sylancr 589	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
148	147	impcom 410	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹))) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))
149	113, 148	anim12i 614	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))) → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
150	149	anassrs 470	. . . . . . . . . . . . . . . . . 18 ⊢ (((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹))) → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
151	150, 135	sylan2 594	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ On ∧ ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
152	151	exp32 423	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ On → ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))))
153		raleq 3406	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑤 → (∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)))
154	153	anbi2d 630	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦))))
155	110, 154	syl5bb 285	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑤 → (∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦))))
156		fveq2 6665	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑤 → (𝑏‘𝑧) = (𝑏‘𝑤))
157		fveq2 6665	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑤 → (𝑐‘𝑧) = (𝑐‘𝑤))
158	156, 157	breq12d 5072	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → ((𝑏‘𝑧)𝑅(𝑐‘𝑧) ↔ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))
159	158	anbi2d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑤 → (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) ↔ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
160	155, 159	anbi12d 632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑤 → ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) ↔ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))))
161	160	imbi1d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑤 → (((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))) ↔ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
162	152, 161	syl5ibcom 247	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ On → (𝑧 = 𝑤 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
163	162	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 = 𝑤 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
164		simp1r 1194	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑤 ∈ On)
165		onelss 6228	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ On → (𝑤 ∈ 𝑧 → 𝑤 ⊆ 𝑧))
166	165	imp 409	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ 𝑧) → 𝑤 ⊆ 𝑧)
167	166	adantlr 713	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧) → 𝑤 ⊆ 𝑧)
168		ssralv 4033	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ⊆ 𝑧 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦)))
169	168	anim1d 612	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ⊆ 𝑧 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦))))
170		r19.26 3170	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ 𝑤 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)))
171	112	ralimi 3160	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ 𝑤 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦))
172	170, 171	sylbir 237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦))
173	169, 172	syl6 35	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ⊆ 𝑧 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
174	173	adantrd 494	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ⊆ 𝑧 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
175	167, 174	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
176	175	3impia 1113	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦))
177		fveq2 6665	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑤 → (𝑎‘𝑦) = (𝑎‘𝑤))
178		fveq2 6665	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑤 → (𝑏‘𝑦) = (𝑏‘𝑤))
179	177, 178	eqeq12d 2837	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑤 → ((𝑎‘𝑦) = (𝑏‘𝑦) ↔ (𝑎‘𝑤) = (𝑏‘𝑤)))
180	179	rspcv 3618	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ 𝑧 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑤) = (𝑏‘𝑤)))
181		breq1 5062	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎‘𝑤) = (𝑏‘𝑤) → ((𝑎‘𝑤)𝑅(𝑐‘𝑤) ↔ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))
182	181	biimprd 250	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎‘𝑤) = (𝑏‘𝑤) → ((𝑏‘𝑤)𝑅(𝑐‘𝑤) → (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
183	180, 182	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ 𝑧 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → ((𝑏‘𝑤)𝑅(𝑐‘𝑤) → (𝑎‘𝑤)𝑅(𝑐‘𝑤))))
184	183	com3l 89	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → ((𝑏‘𝑤)𝑅(𝑐‘𝑤) → (𝑤 ∈ 𝑧 → (𝑎‘𝑤)𝑅(𝑐‘𝑤))))
185	184	imp 409	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)) → (𝑤 ∈ 𝑧 → (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
186	185	ad2ant2rl 747	. . . . . . . . . . . . . . . . . . 19 ⊢ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (𝑤 ∈ 𝑧 → (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
187	186	impcom 410	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑤)𝑅(𝑐‘𝑤))
188	187	3adant1 1126	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑤)𝑅(𝑐‘𝑤))
189		raleq 3406	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑤 → (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
190		fveq2 6665	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑤 → (𝑎‘𝑡) = (𝑎‘𝑤))
191		fveq2 6665	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑤 → (𝑐‘𝑡) = (𝑐‘𝑤))
192	190, 191	breq12d 5072	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑤 → ((𝑎‘𝑡)𝑅(𝑐‘𝑡) ↔ (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
193	189, 192	anbi12d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑤 → ((∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)) ↔ (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑤)𝑅(𝑐‘𝑤))))
194	193	rspcev 3623	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ On ∧ (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑤)𝑅(𝑐‘𝑤))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
195	164, 176, 188, 194	syl12anc 834	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
196	195	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
197	196	3exp 1115	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑤 ∈ 𝑧 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
198	138, 163, 197	3jaod 1424	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → ((𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
199	103, 198	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))))
200	199	rexlimivv 3292	. . . . . . . . . . 11 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
201	99, 200	sylbir 237	. . . . . . . . . 10 ⊢ ((∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
202	201	impcom 410	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
203	94, 95, 202	jca31 517	. . . . . . . 8 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
204	203	an4s 658	. . . . . . 7 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))) ∧ ((𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
205	64, 93, 204	syl2anb 599	. . . . . 6 ⊢ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
206		raleq 3406	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦)))
207		fveq2 6665	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → (𝑓‘𝑥) = (𝑓‘𝑡))
208		fveq2 6665	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → (𝑔‘𝑥) = (𝑔‘𝑡))
209	207, 208	breq12d 5072	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑓‘𝑡)𝑅(𝑔‘𝑡)))
210	206, 209	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = 𝑡 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡))))
211	210	cbvrexvw 3451	. . . . . . . . 9 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡)))
212	20	ralbidv 3197	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦)))
213		fveq1 6664	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑡) = (𝑎‘𝑡))
214	213	breq1d 5069	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑡)𝑅(𝑔‘𝑡) ↔ (𝑎‘𝑡)𝑅(𝑔‘𝑡)))
215	212, 214	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡)) ↔ (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))))
216	215	rexbidv 3297	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → (∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))))
217	211, 216	syl5bb 285	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))))
218	18, 217	anbi12d 632	. . . . . . 7 ⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡)))))
219	83	anbi2d 630	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))
220	85	eqeq2d 2832	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑐‘𝑦)))
221	220	ralbidv 3197	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦)))
222		fveq1 6664	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → (𝑔‘𝑡) = (𝑐‘𝑡))
223	222	breq2d 5071	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → ((𝑎‘𝑡)𝑅(𝑔‘𝑡) ↔ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
224	221, 223	anbi12d 632	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → ((∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡)) ↔ (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
225	224	rexbidv 3297	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
226	219, 225	anbi12d 632	. . . . . . 7 ⊢ (𝑔 = 𝑐 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))))
227	16, 65, 218, 226, 37	brab 5423	. . . . . 6 ⊢ (𝑎𝑆𝑐 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
228	205, 227	sylibr 236	. . . . 5 ⊢ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)
229	39, 228	pm3.2i 473	. . . 4 ⊢ (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐))
230	229	a1i 11	. . 3 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) → (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
231	230	rgen3 3204	. 2 ⊢ ∀𝑎 ∈ 𝐹 ∀𝑏 ∈ 𝐹 ∀𝑐 ∈ 𝐹 (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐))
232		df-po 5469	. 2 ⊢ (𝑆 Po 𝐹 ↔ ∀𝑎 ∈ 𝐹 ∀𝑏 ∈ 𝐹 ∀𝑐 ∈ 𝐹 (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
233	231, 232	mpbir 233	1 ⊢ 𝑆 Po 𝐹

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∨ w3o 1082   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110  {cab 2799  ∀wral 3138  ∃wrex 3139   ∪ cun 3934   ⊆ wss 3936  ∅c0 4291  {csn 4561   class class class wbr 5059  {copab 5121   Po wpo 5467  Ord word 6185  Oncon0 6186  ⟶wf 6346  ‘cfv 6350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-opab 5122  df-tr 5166  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-we 5511  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-ord 6189  df-on 6190  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-fv 6358

This theorem is referenced by:  soseq  33091