ttrclss - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ttrclss		Structured version Visualization version GIF version

Theorem ttrclss 9717

Description: If 𝑅 is a subclass of 𝑆 and 𝑆 is transitive, then the transitive closure of 𝑅 is a subclass of 𝑆. (Contributed by Scott Fenton, 20-Oct-2024.)

**Assertion**
Ref	Expression
ttrclss	⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → t++𝑅 ⊆ 𝑆)

Proof of Theorem ttrclss Dummy variables 𝑥 𝑦 𝑧 𝑓 𝑔 𝑛 𝑚 𝑎 𝑏 𝑖 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		suceq 6429	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → suc 𝑚 = suc ∅)
2		suceq 6429	. . . . . . . . . . . . . . 15 ⊢ (suc 𝑚 = suc ∅ → suc suc 𝑚 = suc suc ∅)
3	1, 2	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → suc suc 𝑚 = suc suc ∅)
4	3	fneq2d 6642	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc ∅))
5		df-1o 8468	. . . . . . . . . . . . . . . 16 ⊢ 1_o = suc ∅
6	1, 5	eqtr4di 2788	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → suc 𝑚 = 1_o)
7	6	fveqeq2d 6898	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘1_o) = 𝑦))
8	7	anbi2d 627	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦)))
9		df1o2 8475	. . . . . . . . . . . . . . . 16 ⊢ 1_o = {∅}
10	6, 9	eqtrdi 2786	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → suc 𝑚 = {∅})
11	10	raleqdv 3323	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ {∅} (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
12		0ex 5306	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ V
13		fveq2 6890	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∅ → (𝑓‘𝑎) = (𝑓‘∅))
14		suceq 6429	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = ∅ → suc 𝑎 = suc ∅)
15	14, 5	eqtr4di 2788	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∅ → suc 𝑎 = 1_o)
16	15	fveq2d 6894	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∅ → (𝑓‘suc 𝑎) = (𝑓‘1_o))
17	13, 16	breq12d 5160	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = ∅ → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∅)𝑅(𝑓‘1_o)))
18	12, 17	ralsn 4684	. . . . . . . . . . . . . 14 ⊢ (∀𝑎 ∈ {∅} (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∅)𝑅(𝑓‘1_o))
19	11, 18	bitrdi 286	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∅)𝑅(𝑓‘1_o)))
20	4, 8, 19	3anbi123d 1434	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o))))
21	20	exbidv 1922	. . . . . . . . . . 11 ⊢ (𝑚 = ∅ → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o))))
22	21	imbi1d 340	. . . . . . . . . 10 ⊢ (𝑚 = ∅ → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑆𝑦)))
23	22	albidv 1921	. . . . . . . . 9 ⊢ (𝑚 = ∅ → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑆𝑦)))
24	23	imbi2d 339	. . . . . . . 8 ⊢ (𝑚 = ∅ → (((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)) ↔ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑆𝑦))))
25		suceq 6429	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑖 → suc 𝑚 = suc 𝑖)
26		suceq 6429	. . . . . . . . . . . . . . . . 17 ⊢ (suc 𝑚 = suc 𝑖 → suc suc 𝑚 = suc suc 𝑖)
27	25, 26	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → suc suc 𝑚 = suc suc 𝑖)
28	27	fneq2d 6642	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc 𝑖))
29	25	fveqeq2d 6898	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘suc 𝑖) = 𝑦))
30	29	anbi2d 627	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦)))
31	25	raleqdv 3323	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
32		fveq2 6890	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → (𝑓‘𝑎) = (𝑓‘𝑏))
33		suceq 6429	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑏 → suc 𝑎 = suc 𝑏)
34	33	fveq2d 6894	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → (𝑓‘suc 𝑎) = (𝑓‘suc 𝑏))
35	32, 34	breq12d 5160	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘𝑏)𝑅(𝑓‘suc 𝑏)))
36	35	cbvralvw 3232	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑎 ∈ suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏))
37	31, 36	bitrdi 286	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏)))
38	28, 30, 37	3anbi123d 1434	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑖 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏))))
39	38	exbidv 1922	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏))))
40		fneq1 6639	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (𝑓 Fn suc suc 𝑖 ↔ 𝑔 Fn suc suc 𝑖))
41		fveq1 6889	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘∅) = (𝑔‘∅))
42	41	eqeq1d 2732	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((𝑓‘∅) = 𝑥 ↔ (𝑔‘∅) = 𝑥))
43		fveq1 6889	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘suc 𝑖) = (𝑔‘suc 𝑖))
44	43	eqeq1d 2732	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((𝑓‘suc 𝑖) = 𝑦 ↔ (𝑔‘suc 𝑖) = 𝑦))
45	42, 44	anbi12d 629	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ↔ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦)))
46		fveq1 6889	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑏) = (𝑔‘𝑏))
47		fveq1 6889	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘suc 𝑏) = (𝑔‘suc 𝑏))
48	46, 47	breq12d 5160	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑏)𝑅(𝑓‘suc 𝑏) ↔ (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
49	48	ralbidv 3175	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏) ↔ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
50	40, 45, 49	3anbi123d 1434	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → ((𝑓 Fn suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏)) ↔ (𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
51	50	cbvexvw 2038	. . . . . . . . . . . . 13 ⊢ (∃𝑓(𝑓 Fn suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
52	39, 51	bitrdi 286	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑖 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
53	52	imbi1d 340	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑖 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑦)))
54	53	albidv 1921	. . . . . . . . . 10 ⊢ (𝑚 = 𝑖 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑦)))
55		eqeq2 2742	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → ((𝑔‘suc 𝑖) = 𝑦 ↔ (𝑔‘suc 𝑖) = 𝑧))
56	55	anbi2d 627	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → (((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ↔ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧)))
57	56	3anbi2d 1439	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → ((𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) ↔ (𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
58	57	exbidv 1922	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
59		breq2 5151	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑥𝑆𝑦 ↔ 𝑥𝑆𝑧))
60	58, 59	imbi12d 343	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑦) ↔ (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)))
61	60	cbvalvw 2037	. . . . . . . . . 10 ⊢ (∀𝑦(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑦) ↔ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧))
62	54, 61	bitrdi 286	. . . . . . . . 9 ⊢ (𝑚 = 𝑖 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)))
63	62	imbi2d 339	. . . . . . . 8 ⊢ (𝑚 = 𝑖 → (((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)) ↔ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧))))
64		suceq 6429	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = suc 𝑖 → suc 𝑚 = suc suc 𝑖)
65		suceq 6429	. . . . . . . . . . . . . . 15 ⊢ (suc 𝑚 = suc suc 𝑖 → suc suc 𝑚 = suc suc suc 𝑖)
66	64, 65	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑚 = suc 𝑖 → suc suc 𝑚 = suc suc suc 𝑖)
67	66	fneq2d 6642	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc suc 𝑖))
68	64	fveqeq2d 6898	. . . . . . . . . . . . . 14 ⊢ (𝑚 = suc 𝑖 → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘suc suc 𝑖) = 𝑦))
69	68	anbi2d 627	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦)))
70	64	raleqdv 3323	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
71	67, 69, 70	3anbi123d 1434	. . . . . . . . . . . 12 ⊢ (𝑚 = suc 𝑖 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
72	71	exbidv 1922	. . . . . . . . . . 11 ⊢ (𝑚 = suc 𝑖 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
73	72	imbi1d 340	. . . . . . . . . 10 ⊢ (𝑚 = suc 𝑖 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
74	73	albidv 1921	. . . . . . . . 9 ⊢ (𝑚 = suc 𝑖 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
75	74	imbi2d 339	. . . . . . . 8 ⊢ (𝑚 = suc 𝑖 → (((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)) ↔ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))))
76		suceq 6429	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑛 → suc 𝑚 = suc 𝑛)
77		suceq 6429	. . . . . . . . . . . . . . 15 ⊢ (suc 𝑚 = suc 𝑛 → suc suc 𝑚 = suc suc 𝑛)
78	76, 77	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → suc suc 𝑚 = suc suc 𝑛)
79	78	fneq2d 6642	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc 𝑛))
80	76	fveqeq2d 6898	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘suc 𝑛) = 𝑦))
81	80	anbi2d 627	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦)))
82	76	raleqdv 3323	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
83	79, 81, 82	3anbi123d 1434	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
84	83	exbidv 1922	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
85	84	imbi1d 340	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
86	85	albidv 1921	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
87	86	imbi2d 339	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)) ↔ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))))
88		breq12 5152	. . . . . . . . . . . . 13 ⊢ (((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) → ((𝑓‘∅)𝑅(𝑓‘1_o) ↔ 𝑥𝑅𝑦))
89	88	biimpa 475	. . . . . . . . . . . 12 ⊢ ((((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑅𝑦)
90	89	3adant1 1128	. . . . . . . . . . 11 ⊢ ((𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑅𝑦)
91		ssbr 5191	. . . . . . . . . . . 12 ⊢ (𝑅 ⊆ 𝑆 → (𝑥𝑅𝑦 → 𝑥𝑆𝑦))
92	91	adantr 479	. . . . . . . . . . 11 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → (𝑥𝑅𝑦 → 𝑥𝑆𝑦))
93	90, 92	syl5 34	. . . . . . . . . 10 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ((𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑆𝑦))
94	93	exlimdv 1934	. . . . . . . . 9 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → (∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑆𝑦))
95	94	alrimiv 1928	. . . . . . . 8 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑆𝑦))
96		fvex 6903	. . . . . . . . . . . . . . 15 ⊢ (𝑓‘suc 𝑖) ∈ V
97		eqeq2 2742	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘suc 𝑖) → ((𝑔‘suc 𝑖) = 𝑧 ↔ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)))
98	97	anbi2d 627	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑓‘suc 𝑖) → (((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ↔ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖))))
99	98	3anbi2d 1439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑓‘suc 𝑖) → ((𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) ↔ (𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
100	99	exbidv 1922	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑓‘suc 𝑖) → (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
101		breq2 5151	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑓‘suc 𝑖) → (𝑥𝑆𝑧 ↔ 𝑥𝑆(𝑓‘suc 𝑖)))
102	100, 101	imbi12d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑓‘suc 𝑖) → ((∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧) ↔ (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆(𝑓‘suc 𝑖))))
103	96, 102	spcv 3594	. . . . . . . . . . . . . 14 ⊢ (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧) → (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆(𝑓‘suc 𝑖)))
104		simpr1 1192	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → 𝑓 Fn suc suc suc 𝑖)
105		sssucid 6443	. . . . . . . . . . . . . . . . . . 19 ⊢ suc suc 𝑖 ⊆ suc suc suc 𝑖
106		fnssres 6672	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 Fn suc suc suc 𝑖 ∧ suc suc 𝑖 ⊆ suc suc suc 𝑖) → (𝑓 ↾ suc suc 𝑖) Fn suc suc 𝑖)
107	104, 105, 106	sylancl 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓 ↾ suc suc 𝑖) Fn suc suc 𝑖)
108		peano2 7883	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ ω → suc 𝑖 ∈ ω)
109	108	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → suc 𝑖 ∈ ω)
110		nnord 7865	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc 𝑖 ∈ ω → Ord suc 𝑖)
111	109, 110	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → Ord suc 𝑖)
112		0elsuc 7825	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Ord suc 𝑖 → ∅ ∈ suc suc 𝑖)
113	111, 112	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∅ ∈ suc suc 𝑖)
114	113	fvresd 6910	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ((𝑓 ↾ suc suc 𝑖)‘∅) = (𝑓‘∅))
115		simpr2l 1230	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∅) = 𝑥)
116	114, 115	eqtrd 2770	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥)
117		vex 3476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑖 ∈ V
118	117	sucex 7796	. . . . . . . . . . . . . . . . . . . 20 ⊢ suc 𝑖 ∈ V
119	118	sucid 6445	. . . . . . . . . . . . . . . . . . 19 ⊢ suc 𝑖 ∈ suc suc 𝑖
120		fvres 6909	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑖 ∈ suc suc 𝑖 → ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖) = (𝑓‘suc 𝑖))
121	119, 120	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖) = (𝑓‘suc 𝑖))
122		simplr3 1215	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))
123		elelsuc 6436	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 ∈ suc 𝑖 → 𝑏 ∈ suc suc 𝑖)
124	123	adantl 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → 𝑏 ∈ suc suc 𝑖)
125	35, 122, 124	rspcdva 3612	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → (𝑓‘𝑏)𝑅(𝑓‘suc 𝑏))
126	124	fvresd 6910	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ((𝑓 ↾ suc suc 𝑖)‘𝑏) = (𝑓‘𝑏))
127		ordsucelsuc 7812	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord suc 𝑖 → (𝑏 ∈ suc 𝑖 ↔ suc 𝑏 ∈ suc suc 𝑖))
128	111, 127	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑏 ∈ suc 𝑖 ↔ suc 𝑏 ∈ suc suc 𝑖))
129	128	biimpa 475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → suc 𝑏 ∈ suc suc 𝑖)
130	129	fvresd 6910	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ((𝑓 ↾ suc suc 𝑖)‘suc 𝑏) = (𝑓‘suc 𝑏))
131	125, 126, 130	3brtr4d 5179	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏))
132	131	ralrimiva 3144	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑏 ∈ suc 𝑖((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏))
133		vex 3476	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑓 ∈ V
134	133	resex 6028	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ↾ suc suc 𝑖) ∈ V
135		fneq1 6639	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔 Fn suc suc 𝑖 ↔ (𝑓 ↾ suc suc 𝑖) Fn suc suc 𝑖))
136		fveq1 6889	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘∅) = ((𝑓 ↾ suc suc 𝑖)‘∅))
137	136	eqeq1d 2732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → ((𝑔‘∅) = 𝑥 ↔ ((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥))
138		fveq1 6889	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘suc 𝑖) = ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖))
139	138	eqeq1d 2732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → ((𝑔‘suc 𝑖) = (𝑓‘suc 𝑖) ↔ ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖) = (𝑓‘suc 𝑖)))
140	137, 139	anbi12d 629	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ↔ (((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥 ∧ ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖) = (𝑓‘suc 𝑖))))
141		fveq1 6889	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘𝑏) = ((𝑓 ↾ suc suc 𝑖)‘𝑏))
142		fveq1 6889	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘suc 𝑏) = ((𝑓 ↾ suc suc 𝑖)‘suc 𝑏))
143	141, 142	breq12d 5160	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → ((𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ ((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏)))
144	143	ralbidv 3175	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ ∀𝑏 ∈ suc 𝑖((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏)))
145	135, 140, 144	3anbi123d 1434	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → ((𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) ↔ ((𝑓 ↾ suc suc 𝑖) Fn suc suc 𝑖 ∧ (((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥 ∧ ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏))))
146	134, 145	spcev 3595	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ↾ suc suc 𝑖) Fn suc suc 𝑖 ∧ (((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥 ∧ ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏)) → ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
147	107, 116, 121, 132, 146	syl121anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
148		simplrl 773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → 𝑅 ⊆ 𝑆)
149		simpr3 1194	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))
150		ssbr 5191	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ⊆ 𝑆 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) → (𝑓‘𝑎)𝑆(𝑓‘suc 𝑎)))
151	150	ralimdv 3167	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ⊆ 𝑆 → (∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) → ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑆(𝑓‘suc 𝑎)))
152	148, 149, 151	sylc 65	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑆(𝑓‘suc 𝑎))
153		fveq2 6890	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = suc 𝑖 → (𝑓‘𝑎) = (𝑓‘suc 𝑖))
154		suceq 6429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = suc 𝑖 → suc 𝑎 = suc suc 𝑖)
155	154	fveq2d 6894	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = suc 𝑖 → (𝑓‘suc 𝑎) = (𝑓‘suc suc 𝑖))
156	153, 155	breq12d 5160	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = suc 𝑖 → ((𝑓‘𝑎)𝑆(𝑓‘suc 𝑎) ↔ (𝑓‘suc 𝑖)𝑆(𝑓‘suc suc 𝑖)))
157	156	rspcv 3607	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑖 ∈ suc suc 𝑖 → (∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑆(𝑓‘suc 𝑎) → (𝑓‘suc 𝑖)𝑆(𝑓‘suc suc 𝑖)))
158	119, 152, 157	mpsyl 68	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc 𝑖)𝑆(𝑓‘suc suc 𝑖))
159		simpr2r 1231	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc suc 𝑖) = 𝑦)
160	158, 159	breqtrd 5173	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc 𝑖)𝑆𝑦)
161		breq1 5150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = (𝑓‘suc 𝑖) → (𝑧𝑆𝑦 ↔ (𝑓‘suc 𝑖)𝑆𝑦))
162	101, 161	anbi12d 629	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = (𝑓‘suc 𝑖) → ((𝑥𝑆𝑧 ∧ 𝑧𝑆𝑦) ↔ (𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦)))
163	96, 162	spcev 3595	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦) → ∃𝑧(𝑥𝑆𝑧 ∧ 𝑧𝑆𝑦))
164		vex 3476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
165		vex 3476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
166	164, 165	brco 5869	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥(𝑆 ∘ 𝑆)𝑦 ↔ ∃𝑧(𝑥𝑆𝑧 ∧ 𝑧𝑆𝑦))
167	163, 166	sylibr 233	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦) → 𝑥(𝑆 ∘ 𝑆)𝑦)
168		simplrr 774	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑆 ∘ 𝑆) ⊆ 𝑆)
169	168	ssbrd 5190	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑥(𝑆 ∘ 𝑆)𝑦 → 𝑥𝑆𝑦))
170	167, 169	syl5 34	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ((𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦) → 𝑥𝑆𝑦))
171	160, 170	mpan2d 690	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑥𝑆(𝑓‘suc 𝑖) → 𝑥𝑆𝑦))
172	147, 171	embantd 59	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ((∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆(𝑓‘suc 𝑖)) → 𝑥𝑆𝑦))
173	172	ex 411	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) → ((𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → ((∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆(𝑓‘suc 𝑖)) → 𝑥𝑆𝑦)))
174	173	com23 86	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) → ((∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆(𝑓‘suc 𝑖)) → ((𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
175	103, 174	syl5 34	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) → (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧) → ((𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
176	175	3impia 1115	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)) → ((𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
177	176	exlimdv 1934	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)) → (∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
178	177	alrimiv 1928	. . . . . . . . . 10 ⊢ ((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
179	178	3exp 1117	. . . . . . . . 9 ⊢ (𝑖 ∈ ω → ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))))
180	179	a2d 29	. . . . . . . 8 ⊢ (𝑖 ∈ ω → (((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)) → ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))))
181	24, 63, 75, 87, 95, 180	finds 7891	. . . . . . 7 ⊢ (𝑛 ∈ ω → ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
182	181	com12 32	. . . . . 6 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → (𝑛 ∈ ω → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
183	182	ralrimiv 3143	. . . . 5 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑛 ∈ ω ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
184		ralcom4 3281	. . . . . 6 ⊢ (∀𝑛 ∈ ω ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦∀𝑛 ∈ ω (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
185		r19.23v 3180	. . . . . . 7 ⊢ (∀𝑛 ∈ ω (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
186	185	albii 1819	. . . . . 6 ⊢ (∀𝑦∀𝑛 ∈ ω (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
187	184, 186	bitri 274	. . . . 5 ⊢ (∀𝑛 ∈ ω ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
188	183, 187	sylib 217	. . . 4 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
189		brttrcl2 9711	. . . . . . 7 ⊢ (𝑥t++𝑅𝑦 ↔ ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
190		df-br 5148	. . . . . . 7 ⊢ (𝑥t++𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
191	189, 190	bitr3i 276	. . . . . 6 ⊢ (∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
192		df-br 5148	. . . . . 6 ⊢ (𝑥𝑆𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑆)
193	191, 192	imbi12i 349	. . . . 5 ⊢ ((∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
194	193	albii 1819	. . . 4 ⊢ (∀𝑦(∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
195	188, 194	sylib 217	. . 3 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
196	195	alrimiv 1928	. 2 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
197		relttrcl 9709	. . 3 ⊢ Rel t++𝑅
198		ssrel 5781	. . 3 ⊢ (Rel t++𝑅 → (t++𝑅 ⊆ 𝑆 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆)))
199	197, 198	ax-mp 5	. 2 ⊢ (t++𝑅 ⊆ 𝑆 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
200	196, 199	sylibr 233	1 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → t++𝑅 ⊆ 𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1085 ∀wal 1537 = wceq 1539 ∃wex 1779 ∈ wcel 2104 ∀wral 3059 ∃wrex 3068 ⊆ wss 3947 ∅c0 4321 {csn 4627 ⟨cop 4633 class class class wbr 5147 ↾ cres 5677 ∘ ccom 5679 Rel wrel 5680 Ord word 6362 suc csuc 6365 Fn wfn 6537 ‘cfv 6542 ωcom 7857 1_oc1o 8461 t++cttrcl 9704

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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pr 5426 ax-un 7727

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-ral 3060 df-rex 3069 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-2nd 7978 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-oadd 8472 df-ttrcl 9705

This theorem is referenced by: dfttrcl2 9721

W3C validator