Theorem poseq 8162

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 6692	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑏 → (𝑓:𝑥⟶𝐴 ↔ 𝑓:𝑏⟶𝐴))
4	3	cbvrexvw 3225	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥 ∈ On 𝑓:𝑥⟶𝐴 ↔ ∃𝑏 ∈ On 𝑓:𝑏⟶𝐴)
5	4	abbii 2803	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏⟶𝐴}
6	2, 5	eqtri 2759	. . . . . . . . . . . . 13 ⊢ 𝐹 = {𝑓 ∣ ∃𝑏 ∈ On 𝑓:𝑏⟶𝐴}
7	6	orderseqlem 8161	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝐹 → (𝑎‘𝑥) ∈ (𝐴 ∪ {∅}))
8		poirr 5578	. . . . . . . . . . . 12 ⊢ ((𝑅 Po (𝐴 ∪ {∅}) ∧ (𝑎‘𝑥) ∈ (𝐴 ∪ {∅})) → ¬ (𝑎‘𝑥)𝑅(𝑎‘𝑥))
9	1, 7, 8	sylancr 587	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝐹 → ¬ (𝑎‘𝑥)𝑅(𝑎‘𝑥))
10	9	intnand 488	. . . . . . . . . 10 ⊢ (𝑎 ∈ 𝐹 → ¬ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
11	10	adantr 480	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑥 ∈ On) → ¬ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
12	11	nrexdv 3136	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐹 → ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
13	12	adantr 480	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
14		imnan 399	. . . . . . 7 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))) ↔ ¬ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
15	13, 14	mpbi 230	. . . . . 6 ⊢ ¬ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
16		vex 3468	. . . . . . 7 ⊢ 𝑎 ∈ V
17		eleq1w 2818	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → (𝑓 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹))
18	17	anbi1d 631	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹)))
19		fveq1 6880	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑦) = (𝑎‘𝑦))
20	19	eqeq1d 2738	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑔‘𝑦)))
21	20	ralbidv 3164	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦)))
22		fveq1 6880	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑥) = (𝑎‘𝑥))
23	22	breq1d 5134	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))
24	21, 23	anbi12d 632	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))))
25	24	rexbidv 3165	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))))
26	18, 25	anbi12d 632	. . . . . . 7 ⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))))
27		eleq1w 2818	. . . . . . . . 9 ⊢ (𝑔 = 𝑎 → (𝑔 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹))
28	27	anbi2d 630	. . . . . . . 8 ⊢ (𝑔 = 𝑎 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹)))
29		fveq1 6880	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑦) = (𝑎‘𝑦))
30	29	eqeq2d 2747	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑎 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑎‘𝑦)))
31	30	ralbidv 3164	. . . . . . . . . 10 ⊢ (𝑔 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦)))
32		fveq1 6880	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑥) = (𝑎‘𝑥))
33	32	breq2d 5136	. . . . . . . . . 10 ⊢ (𝑔 = 𝑎 → ((𝑎‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))
34	31, 33	anbi12d 632	. . . . . . . . 9 ⊢ (𝑔 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
35	34	rexbidv 3165	. . . . . . . 8 ⊢ (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
36	28, 35	anbi12d 632	. . . . . . 7 ⊢ (𝑔 = 𝑎 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥)))))
37		poseq.3	. . . . . . 7 ⊢ 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))}
38	16, 16, 26, 36, 37	brab 5523	. . . . . 6 ⊢ (𝑎𝑆𝑎 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑎‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑎‘𝑥))))
39	15, 38	mtbir 323	. . . . 5 ⊢ ¬ 𝑎𝑆𝑎
40		vex 3468	. . . . . . . 8 ⊢ 𝑏 ∈ V
41		raleq 3306	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦)))
42		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑓‘𝑥) = (𝑓‘𝑧))
43		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑔‘𝑥) = (𝑔‘𝑧))
44	42, 43	breq12d 5137	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑓‘𝑧)𝑅(𝑔‘𝑧)))
45	41, 44	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧))))
46	45	cbvrexvw 3225	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧)))
47	20	ralbidv 3164	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦)))
48		fveq1 6880	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑧) = (𝑎‘𝑧))
49	48	breq1d 5134	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑧)𝑅(𝑔‘𝑧) ↔ (𝑎‘𝑧)𝑅(𝑔‘𝑧)))
50	47, 49	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))))
51	50	rexbidv 3165	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑧)𝑅(𝑔‘𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))))
52	46, 51	bitrid 283	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))))
53	18, 52	anbi12d 632	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧)))))
54		eleq1w 2818	. . . . . . . . . 10 ⊢ (𝑔 = 𝑏 → (𝑔 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹))
55	54	anbi2d 630	. . . . . . . . 9 ⊢ (𝑔 = 𝑏 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹)))
56		fveq1 6880	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑦) = (𝑏‘𝑦))
57	56	eqeq2d 2747	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑏 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑏‘𝑦)))
58	57	ralbidv 3164	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑏 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦)))
59		fveq1 6880	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑧) = (𝑏‘𝑧))
60	59	breq2d 5136	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑏 → ((𝑎‘𝑧)𝑅(𝑔‘𝑧) ↔ (𝑎‘𝑧)𝑅(𝑏‘𝑧)))
61	58, 60	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑔 = 𝑏 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))))
62	61	rexbidv 3165	. . . . . . . . 9 ⊢ (𝑔 = 𝑏 → (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧)) ↔ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))))
63	55, 62	anbi12d 632	. . . . . . . 8 ⊢ (𝑔 = 𝑏 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑔‘𝑧))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)))))
64	16, 40, 53, 63, 37	brab 5523	. . . . . . 7 ⊢ (𝑎𝑆𝑏 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))))
65		vex 3468	. . . . . . . 8 ⊢ 𝑐 ∈ V
66		eleq1w 2818	. . . . . . . . . 10 ⊢ (𝑓 = 𝑏 → (𝑓 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹))
67	66	anbi1d 631	. . . . . . . . 9 ⊢ (𝑓 = 𝑏 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹)))
68		raleq 3306	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦)))
69		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → (𝑓‘𝑥) = (𝑓‘𝑤))
70		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → (𝑔‘𝑥) = (𝑔‘𝑤))
71	69, 70	breq12d 5137	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑓‘𝑤)𝑅(𝑔‘𝑤)))
72	68, 71	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤))))
73	72	cbvrexvw 3225	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤)))
74		fveq1 6880	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑦) = (𝑏‘𝑦))
75	74	eqeq1d 2738	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑔‘𝑦)))
76	75	ralbidv 3164	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦)))
77		fveq1 6880	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑤) = (𝑏‘𝑤))
78	77	breq1d 5134	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑤)𝑅(𝑔‘𝑤) ↔ (𝑏‘𝑤)𝑅(𝑔‘𝑤)))
79	76, 78	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑏 → ((∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤)) ↔ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))))
80	79	rexbidv 3165	. . . . . . . . . 10 ⊢ (𝑓 = 𝑏 → (∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑤)𝑅(𝑔‘𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))))
81	73, 80	bitrid 283	. . . . . . . . 9 ⊢ (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))))
82	67, 81	anbi12d 632	. . . . . . . 8 ⊢ (𝑓 = 𝑏 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤)))))
83		eleq1w 2818	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → (𝑔 ∈ 𝐹 ↔ 𝑐 ∈ 𝐹))
84	83	anbi2d 630	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))
85		fveq1 6880	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑐 → (𝑔‘𝑦) = (𝑐‘𝑦))
86	85	eqeq2d 2747	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑐 → ((𝑏‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑐‘𝑦)))
87	86	ralbidv 3164	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)))
88		fveq1 6880	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑐 → (𝑔‘𝑤) = (𝑐‘𝑤))
89	88	breq2d 5136	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → ((𝑏‘𝑤)𝑅(𝑔‘𝑤) ↔ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))
90	87, 89	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → ((∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤)) ↔ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
91	90	rexbidv 3165	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → (∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤)) ↔ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
92	84, 91	anbi12d 632	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑔‘𝑤))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))))
93	40, 65, 82, 92, 37	brab 5523	. . . . . . 7 ⊢ (𝑏𝑆𝑐 ↔ ((𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
94		simplll 774	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑎 ∈ 𝐹)
95		simplrr 777	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑐 ∈ 𝐹)
96		an4 656	. . . . . . . . . . . . 13 ⊢ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
97	96	2rexbii 3117	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ ∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
98		reeanv 3217	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
99	97, 98	bitri 275	. . . . . . . . . . 11 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) ↔ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
100		eloni 6367	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ On → Ord 𝑧)
101		eloni 6367	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ On → Ord 𝑤)
102		ordtri3or 6389	. . . . . . . . . . . . . 14 ⊢ ((Ord 𝑧 ∧ Ord 𝑤) → (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))
103	100, 101, 102	syl2an 596	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧))
104		simp1l 1198	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑧 ∈ On)
105		onelss 6399	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ On → (𝑧 ∈ 𝑤 → 𝑧 ⊆ 𝑤))
106	105	imp 406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤 ∈ On ∧ 𝑧 ∈ 𝑤) → 𝑧 ⊆ 𝑤)
107	106	adantll 714	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤) → 𝑧 ⊆ 𝑤)
108		ssralv 4032	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ⊆ 𝑤 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦)))
109	108	anim2d 612	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ⊆ 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦))))
110		r19.26 3099	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦)))
111	109, 110	imbitrrdi 252	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ⊆ 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦))))
112		eqtr 2756	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) → (𝑎‘𝑦) = (𝑐‘𝑦))
113	112	ralimi 3074	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦))
114	111, 113	syl6 35	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ⊆ 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
115	107, 114	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤) → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
116	115	adantrd 491	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
117	116	3impia 1117	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦))
118		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑧 → (𝑏‘𝑦) = (𝑏‘𝑧))
119		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑧 → (𝑐‘𝑦) = (𝑐‘𝑧))
120	118, 119	eqeq12d 2752	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑧 → ((𝑏‘𝑦) = (𝑐‘𝑦) ↔ (𝑏‘𝑧) = (𝑐‘𝑧)))
121	120	rspcv 3602	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ 𝑤 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → (𝑏‘𝑧) = (𝑐‘𝑧)))
122		breq2 5128	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏‘𝑧) = (𝑐‘𝑧) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ↔ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
123	122	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏‘𝑧) = (𝑐‘𝑧) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
124	121, 123	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ 𝑤 → (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))))
125	124	com3l 89	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) → ((𝑎‘𝑧)𝑅(𝑏‘𝑧) → (𝑧 ∈ 𝑤 → (𝑎‘𝑧)𝑅(𝑐‘𝑧))))
126	125	imp 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) → (𝑧 ∈ 𝑤 → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
127	126	ad2ant2lr 748	. . . . . . . . . . . . . . . . . . 19 ⊢ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (𝑧 ∈ 𝑤 → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
128	127	impcom 407	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))
129	128	3adant1 1130	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))
130		raleq 3306	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑧 → (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ↔ ∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦)))
131		fveq2 6881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑧 → (𝑎‘𝑡) = (𝑎‘𝑧))
132		fveq2 6881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑧 → (𝑐‘𝑡) = (𝑐‘𝑧))
133	131, 132	breq12d 5137	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑧 → ((𝑎‘𝑡)𝑅(𝑐‘𝑡) ↔ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
134	130, 133	anbi12d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑧 → ((∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧))))
135	134	rspcev 3606	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ On ∧ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
136	104, 117, 129, 135	syl12anc 836	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
137	136	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑧 ∈ 𝑤 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
138	137	3exp 1119	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ∈ 𝑤 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
139	2	orderseqlem 8161	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ 𝐹 → (𝑎‘𝑧) ∈ (𝐴 ∪ {∅}))
140	139	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (𝑎‘𝑧) ∈ (𝐴 ∪ {∅}))
141	2	orderseqlem 8161	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ∈ 𝐹 → (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}))
142	141	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}))
143	2	orderseqlem 8161	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ 𝐹 → (𝑐‘𝑧) ∈ (𝐴 ∪ {∅}))
144	143	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (𝑐‘𝑧) ∈ (𝐴 ∪ {∅}))
145	140, 142, 144	3jca 1128	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ((𝑎‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐‘𝑧) ∈ (𝐴 ∪ {∅})))
146		potr 5579	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Po (𝐴 ∪ {∅}) ∧ ((𝑎‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑧) ∈ (𝐴 ∪ {∅}) ∧ (𝑐‘𝑧) ∈ (𝐴 ∪ {∅}))) → (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
147	1, 145, 146	sylancr 587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) → (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
148	147	impcom 407	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹))) → (𝑎‘𝑧)𝑅(𝑐‘𝑧))
149	113, 148	anim12i 613	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))) → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
150	149	anassrs 467	. . . . . . . . . . . . . . . . . 18 ⊢ (((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹))) → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑐‘𝑧)))
151	150, 135	sylan2 593	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ On ∧ ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) ∧ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
152	151	exp32 420	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ On → ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))))
153		raleq 3306	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑤 → (∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)))
154	153	anbi2d 630	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑧 (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦))))
155	110, 154	bitrid 283	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑤 → (∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦))))
156		fveq2 6881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑤 → (𝑏‘𝑧) = (𝑏‘𝑤))
157		fveq2 6881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑤 → (𝑐‘𝑧) = (𝑐‘𝑤))
158	156, 157	breq12d 5137	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → ((𝑏‘𝑧)𝑅(𝑐‘𝑧) ↔ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))
159	158	anbi2d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑤 → (((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧)) ↔ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))))
160	155, 159	anbi12d 632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑤 → ((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) ↔ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))))
161	160	imbi1d 341	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑤 → (((∀𝑦 ∈ 𝑧 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑧)𝑅(𝑐‘𝑧))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))) ↔ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
162	152, 161	syl5ibcom 245	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ On → (𝑧 = 𝑤 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
163	162	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 = 𝑤 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
164		simp1r 1199	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → 𝑤 ∈ On)
165		onelss 6399	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ On → (𝑤 ∈ 𝑧 → 𝑤 ⊆ 𝑧))
166	165	imp 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ 𝑧) → 𝑤 ⊆ 𝑧)
167	166	adantlr 715	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧) → 𝑤 ⊆ 𝑧)
168		ssralv 4032	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ⊆ 𝑧 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦)))
169	168	anim1d 611	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ⊆ 𝑧 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦))))
170		r19.26 3099	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ 𝑤 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) ↔ (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)))
171	112	ralimi 3074	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ 𝑤 ((𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦))
172	170, 171	sylbir 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦))
173	169, 172	syl6 35	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ⊆ 𝑧 → ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
174	173	adantrd 491	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ⊆ 𝑧 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
175	167, 174	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
176	175	3impia 1117	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦))
177		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑤 → (𝑎‘𝑦) = (𝑎‘𝑤))
178		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑤 → (𝑏‘𝑦) = (𝑏‘𝑤))
179	177, 178	eqeq12d 2752	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑤 → ((𝑎‘𝑦) = (𝑏‘𝑦) ↔ (𝑎‘𝑤) = (𝑏‘𝑤)))
180	179	rspcv 3602	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ 𝑧 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑤) = (𝑏‘𝑤)))
181		breq1 5127	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎‘𝑤) = (𝑏‘𝑤) → ((𝑎‘𝑤)𝑅(𝑐‘𝑤) ↔ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))
182	181	biimprd 248	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎‘𝑤) = (𝑏‘𝑤) → ((𝑏‘𝑤)𝑅(𝑐‘𝑤) → (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
183	180, 182	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ 𝑧 → (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → ((𝑏‘𝑤)𝑅(𝑐‘𝑤) → (𝑎‘𝑤)𝑅(𝑐‘𝑤))))
184	183	com3l 89	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) → ((𝑏‘𝑤)𝑅(𝑐‘𝑤) → (𝑤 ∈ 𝑧 → (𝑎‘𝑤)𝑅(𝑐‘𝑤))))
185	184	imp 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)) → (𝑤 ∈ 𝑧 → (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
186	185	ad2ant2rl 749	. . . . . . . . . . . . . . . . . . 19 ⊢ (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (𝑤 ∈ 𝑧 → (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
187	186	impcom 407	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑤)𝑅(𝑐‘𝑤))
188	187	3adant1 1130	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (𝑎‘𝑤)𝑅(𝑐‘𝑤))
189		raleq 3306	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑤 → (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦)))
190		fveq2 6881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑤 → (𝑎‘𝑡) = (𝑎‘𝑤))
191		fveq2 6881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑤 → (𝑐‘𝑡) = (𝑐‘𝑤))
192	190, 191	breq12d 5137	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑤 → ((𝑎‘𝑡)𝑅(𝑐‘𝑡) ↔ (𝑎‘𝑤)𝑅(𝑐‘𝑤)))
193	189, 192	anbi12d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑤 → ((∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)) ↔ (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑤)𝑅(𝑐‘𝑤))))
194	193	rspcev 3606	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ On ∧ (∀𝑦 ∈ 𝑤 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑤)𝑅(𝑐‘𝑤))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
195	164, 176, 188, 194	syl12anc 836	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
196	195	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ 𝑤 ∈ 𝑧 ∧ ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
197	196	3exp 1119	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑤 ∈ 𝑧 → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
198	138, 163, 197	3jaod 1431	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → ((𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))))
199	103, 198	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))))
200	199	rexlimivv 3187	. . . . . . . . . . 11 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦)) ∧ ((𝑎‘𝑧)𝑅(𝑏‘𝑧) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
201	99, 200	sylbir 235	. . . . . . . . . 10 ⊢ ((∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤))) → (((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
202	201	impcom 407	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
203	94, 95, 202	jca31 514	. . . . . . . 8 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ (𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)) ∧ (∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧)) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
204	203	an4s 660	. . . . . . 7 ⊢ ((((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑧 ∈ On (∀𝑦 ∈ 𝑧 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑧)𝑅(𝑏‘𝑧))) ∧ ((𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑤 ∈ On (∀𝑦 ∈ 𝑤 (𝑏‘𝑦) = (𝑐‘𝑦) ∧ (𝑏‘𝑤)𝑅(𝑐‘𝑤)))) → ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
205	64, 93, 204	syl2anb 598	. . . . . 6 ⊢ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
206		raleq 3306	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦)))
207		fveq2 6881	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → (𝑓‘𝑥) = (𝑓‘𝑡))
208		fveq2 6881	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → (𝑔‘𝑥) = (𝑔‘𝑡))
209	207, 208	breq12d 5137	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑓‘𝑡)𝑅(𝑔‘𝑡)))
210	206, 209	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = 𝑡 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡))))
211	210	cbvrexvw 3225	. . . . . . . . 9 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡)))
212	20	ralbidv 3164	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦)))
213		fveq1 6880	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑡) = (𝑎‘𝑡))
214	213	breq1d 5134	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑡)𝑅(𝑔‘𝑡) ↔ (𝑎‘𝑡)𝑅(𝑔‘𝑡)))
215	212, 214	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡)) ↔ (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))))
216	215	rexbidv 3165	. . . . . . . . 9 ⊢ (𝑓 = 𝑎 → (∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑡)𝑅(𝑔‘𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))))
217	211, 216	bitrid 283	. . . . . . . 8 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))))
218	18, 217	anbi12d 632	. . . . . . 7 ⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡)))))
219	83	anbi2d 630	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹)))
220	85	eqeq2d 2747	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑐‘𝑦)))
221	220	ralbidv 3164	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦)))
222		fveq1 6880	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑐 → (𝑔‘𝑡) = (𝑐‘𝑡))
223	222	breq2d 5136	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → ((𝑎‘𝑡)𝑅(𝑔‘𝑡) ↔ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))
224	221, 223	anbi12d 632	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → ((∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡)) ↔ (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
225	224	rexbidv 3165	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡)) ↔ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
226	219, 225	anbi12d 632	. . . . . . 7 ⊢ (𝑔 = 𝑐 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑔‘𝑡))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡)))))
227	16, 65, 218, 226, 37	brab 5523	. . . . . 6 ⊢ (𝑎𝑆𝑐 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) ∧ ∃𝑡 ∈ On (∀𝑦 ∈ 𝑡 (𝑎‘𝑦) = (𝑐‘𝑦) ∧ (𝑎‘𝑡)𝑅(𝑐‘𝑡))))
228	205, 227	sylibr 234	. . . . 5 ⊢ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)
229	39, 228	pm3.2i 470	. . . 4 ⊢ (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐))
230	229	a1i 11	. . 3 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹) → (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
231	230	rgen3 3190	. 2 ⊢ ∀𝑎 ∈ 𝐹 ∀𝑏 ∈ 𝐹 ∀𝑐 ∈ 𝐹 (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐))
232		df-po 5566	. 2 ⊢ (𝑆 Po 𝐹 ↔ ∀𝑎 ∈ 𝐹 ∀𝑏 ∈ 𝐹 ∀𝑐 ∈ 𝐹 (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
233	231, 232	mpbir 231	1 ⊢ 𝑆 Po 𝐹

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ w3o 1085   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  {cab 2714  ∀wral 3052  ∃wrex 3061   ∪ cun 3929   ⊆ wss 3931  ∅c0 4313  {csn 4606   class class class wbr 5124  {copab 5186   Po wpo 5564  Ord word 6356  Oncon0 6357  ⟶wf 6532  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-tr 5235  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-ord 6360  df-on 6361  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544

This theorem is referenced by:  soseq  8163