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 9745

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 6437	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → suc 𝑚 = suc ∅)
2		suceq 6437	. . . . . . . . . . . . . . 15 ⊢ (suc 𝑚 = suc ∅ → suc suc 𝑚 = suc suc ∅)
3	1, 2	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → suc suc 𝑚 = suc suc ∅)
4	3	fneq2d 6649	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc ∅))
5		df-1o 8487	. . . . . . . . . . . . . . . 16 ⊢ 1_o = suc ∅
6	1, 5	eqtr4di 2783	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → suc 𝑚 = 1_o)
7	6	fveqeq2d 6904	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘1_o) = 𝑦))
8	7	anbi2d 628	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦)))
9		df1o2 8494	. . . . . . . . . . . . . . . 16 ⊢ 1_o = {∅}
10	6, 9	eqtrdi 2781	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → suc 𝑚 = {∅})
11	10	raleqdv 3314	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ {∅} (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
12		0ex 5308	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ V
13		fveq2 6896	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∅ → (𝑓‘𝑎) = (𝑓‘∅))
14		suceq 6437	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = ∅ → suc 𝑎 = suc ∅)
15	14, 5	eqtr4di 2783	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∅ → suc 𝑎 = 1_o)
16	15	fveq2d 6900	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∅ → (𝑓‘suc 𝑎) = (𝑓‘1_o))
17	13, 16	breq12d 5162	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = ∅ → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∅)𝑅(𝑓‘1_o)))
18	12, 17	ralsn 4687	. . . . . . . . . . . . . 14 ⊢ (∀𝑎 ∈ {∅} (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∅)𝑅(𝑓‘1_o))
19	11, 18	bitrdi 286	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∅)𝑅(𝑓‘1_o)))
20	4, 8, 19	3anbi123d 1432	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o))))
21	20	exbidv 1916	. . . . . . . . . . 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 1915	. . . . . . . . 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 6437	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑖 → suc 𝑚 = suc 𝑖)
26		suceq 6437	. . . . . . . . . . . . . . . . 17 ⊢ (suc 𝑚 = suc 𝑖 → suc suc 𝑚 = suc suc 𝑖)
27	25, 26	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → suc suc 𝑚 = suc suc 𝑖)
28	27	fneq2d 6649	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc 𝑖))
29	25	fveqeq2d 6904	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘suc 𝑖) = 𝑦))
30	29	anbi2d 628	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦)))
31	25	raleqdv 3314	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
32		fveq2 6896	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → (𝑓‘𝑎) = (𝑓‘𝑏))
33		suceq 6437	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑏 → suc 𝑎 = suc 𝑏)
34	33	fveq2d 6900	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → (𝑓‘suc 𝑎) = (𝑓‘suc 𝑏))
35	32, 34	breq12d 5162	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘𝑏)𝑅(𝑓‘suc 𝑏)))
36	35	cbvralvw 3224	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑎 ∈ suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏))
37	31, 36	bitrdi 286	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏)))
38	28, 30, 37	3anbi123d 1432	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑖 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏))))
39	38	exbidv 1916	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏))))
40		fneq1 6646	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (𝑓 Fn suc suc 𝑖 ↔ 𝑔 Fn suc suc 𝑖))
41		fveq1 6895	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘∅) = (𝑔‘∅))
42	41	eqeq1d 2727	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((𝑓‘∅) = 𝑥 ↔ (𝑔‘∅) = 𝑥))
43		fveq1 6895	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘suc 𝑖) = (𝑔‘suc 𝑖))
44	43	eqeq1d 2727	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((𝑓‘suc 𝑖) = 𝑦 ↔ (𝑔‘suc 𝑖) = 𝑦))
45	42, 44	anbi12d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ↔ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦)))
46		fveq1 6895	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑏) = (𝑔‘𝑏))
47		fveq1 6895	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘suc 𝑏) = (𝑔‘suc 𝑏))
48	46, 47	breq12d 5162	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑏)𝑅(𝑓‘suc 𝑏) ↔ (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
49	48	ralbidv 3167	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏) ↔ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
50	40, 45, 49	3anbi123d 1432	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → ((𝑓 Fn suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏)) ↔ (𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
51	50	cbvexvw 2032	. . . . . . . . . . . . 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 1915	. . . . . . . . . 10 ⊢ (𝑚 = 𝑖 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑦)))
55		eqeq2 2737	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → ((𝑔‘suc 𝑖) = 𝑦 ↔ (𝑔‘suc 𝑖) = 𝑧))
56	55	anbi2d 628	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → (((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ↔ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧)))
57	56	3anbi2d 1437	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → ((𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) ↔ (𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
58	57	exbidv 1916	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
59		breq2 5153	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑥𝑆𝑦 ↔ 𝑥𝑆𝑧))
60	58, 59	imbi12d 343	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑦) ↔ (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)))
61	60	cbvalvw 2031	. . . . . . . . . 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 6437	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = suc 𝑖 → suc 𝑚 = suc suc 𝑖)
65		suceq 6437	. . . . . . . . . . . . . . 15 ⊢ (suc 𝑚 = suc suc 𝑖 → suc suc 𝑚 = suc suc suc 𝑖)
66	64, 65	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑚 = suc 𝑖 → suc suc 𝑚 = suc suc suc 𝑖)
67	66	fneq2d 6649	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc suc 𝑖))
68	64	fveqeq2d 6904	. . . . . . . . . . . . . 14 ⊢ (𝑚 = suc 𝑖 → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘suc suc 𝑖) = 𝑦))
69	68	anbi2d 628	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦)))
70	64	raleqdv 3314	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
71	67, 69, 70	3anbi123d 1432	. . . . . . . . . . . 12 ⊢ (𝑚 = suc 𝑖 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
72	71	exbidv 1916	. . . . . . . . . . 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 1915	. . . . . . . . 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 6437	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑛 → suc 𝑚 = suc 𝑛)
77		suceq 6437	. . . . . . . . . . . . . . 15 ⊢ (suc 𝑚 = suc 𝑛 → suc suc 𝑚 = suc suc 𝑛)
78	76, 77	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → suc suc 𝑚 = suc suc 𝑛)
79	78	fneq2d 6649	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc 𝑛))
80	76	fveqeq2d 6904	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘suc 𝑛) = 𝑦))
81	80	anbi2d 628	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦)))
82	76	raleqdv 3314	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
83	79, 81, 82	3anbi123d 1432	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
84	83	exbidv 1916	. . . . . . . . . . 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 1915	. . . . . . . . 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 5154	. . . . . . . . . . . . 13 ⊢ (((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) → ((𝑓‘∅)𝑅(𝑓‘1_o) ↔ 𝑥𝑅𝑦))
89	88	biimpa 475	. . . . . . . . . . . 12 ⊢ ((((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑅𝑦)
90	89	3adant1 1127	. . . . . . . . . . 11 ⊢ ((𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑅𝑦)
91		ssbr 5193	. . . . . . . . . . . 12 ⊢ (𝑅 ⊆ 𝑆 → (𝑥𝑅𝑦 → 𝑥𝑆𝑦))
92	91	adantr 479	. . . . . . . . . . 11 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → (𝑥𝑅𝑦 → 𝑥𝑆𝑦))
93	90, 92	syl5 34	. . . . . . . . . 10 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ((𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑆𝑦))
94	93	exlimdv 1928	. . . . . . . . 9 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → (∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑆𝑦))
95	94	alrimiv 1922	. . . . . . . 8 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑆𝑦))
96		fvex 6909	. . . . . . . . . . . . . . 15 ⊢ (𝑓‘suc 𝑖) ∈ V
97		eqeq2 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘suc 𝑖) → ((𝑔‘suc 𝑖) = 𝑧 ↔ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)))
98	97	anbi2d 628	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑓‘suc 𝑖) → (((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ↔ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖))))
99	98	3anbi2d 1437	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑓‘suc 𝑖) → ((𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) ↔ (𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
100	99	exbidv 1916	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑓‘suc 𝑖) → (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
101		breq2 5153	. . . . . . . . . . . . . . . 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 3589	. . . . . . . . . . . . . 14 ⊢ (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧) → (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆(𝑓‘suc 𝑖)))
104		simpr1 1191	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → 𝑓 Fn suc suc suc 𝑖)
105		sssucid 6451	. . . . . . . . . . . . . . . . . . 19 ⊢ suc suc 𝑖 ⊆ suc suc suc 𝑖
106		fnssres 6679	. . . . . . . . . . . . . . . . . . 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 7897	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ ω → suc 𝑖 ∈ ω)
109	108	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → suc 𝑖 ∈ ω)
110		nnord 7879	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc 𝑖 ∈ ω → Ord suc 𝑖)
111	109, 110	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → Ord suc 𝑖)
112		0elsuc 7839	. . . . . . . . . . . . . . . . . . . . 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 6916	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ((𝑓 ↾ suc suc 𝑖)‘∅) = (𝑓‘∅))
115		simpr2l 1229	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∅) = 𝑥)
116	114, 115	eqtrd 2765	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥)
117		vex 3465	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑖 ∈ V
118	117	sucex 7810	. . . . . . . . . . . . . . . . . . . 20 ⊢ suc 𝑖 ∈ V
119	118	sucid 6453	. . . . . . . . . . . . . . . . . . 19 ⊢ suc 𝑖 ∈ suc suc 𝑖
120		fvres 6915	. . . . . . . . . . . . . . . . . . 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 1214	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))
123		elelsuc 6444	. . . . . . . . . . . . . . . . . . . . . 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 3607	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → (𝑓‘𝑏)𝑅(𝑓‘suc 𝑏))
126	124	fvresd 6916	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ((𝑓 ↾ suc suc 𝑖)‘𝑏) = (𝑓‘𝑏))
127		ordsucelsuc 7826	. . . . . . . . . . . . . . . . . . . . . . 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 6916	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ((𝑓 ↾ suc suc 𝑖)‘suc 𝑏) = (𝑓‘suc 𝑏))
131	125, 126, 130	3brtr4d 5181	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏))
132	131	ralrimiva 3135	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑏 ∈ suc 𝑖((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏))
133		vex 3465	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑓 ∈ V
134	133	resex 6034	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ↾ suc suc 𝑖) ∈ V
135		fneq1 6646	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔 Fn suc suc 𝑖 ↔ (𝑓 ↾ suc suc 𝑖) Fn suc suc 𝑖))
136		fveq1 6895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘∅) = ((𝑓 ↾ suc suc 𝑖)‘∅))
137	136	eqeq1d 2727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → ((𝑔‘∅) = 𝑥 ↔ ((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥))
138		fveq1 6895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘suc 𝑖) = ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖))
139	138	eqeq1d 2727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → ((𝑔‘suc 𝑖) = (𝑓‘suc 𝑖) ↔ ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖) = (𝑓‘suc 𝑖)))
140	137, 139	anbi12d 630	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ↔ (((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥 ∧ ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖) = (𝑓‘suc 𝑖))))
141		fveq1 6895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘𝑏) = ((𝑓 ↾ suc suc 𝑖)‘𝑏))
142		fveq1 6895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘suc 𝑏) = ((𝑓 ↾ suc suc 𝑖)‘suc 𝑏))
143	141, 142	breq12d 5162	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → ((𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ ((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏)))
144	143	ralbidv 3167	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ ∀𝑏 ∈ suc 𝑖((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏)))
145	135, 140, 144	3anbi123d 1432	. . . . . . . . . . . . . . . . . . 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 3590	. . . . . . . . . . . . . . . . . 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 1372	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
148		simplrl 775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → 𝑅 ⊆ 𝑆)
149		simpr3 1193	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))
150		ssbr 5193	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ⊆ 𝑆 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) → (𝑓‘𝑎)𝑆(𝑓‘suc 𝑎)))
151	150	ralimdv 3158	. . . . . . . . . . . . . . . . . . . . 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 6896	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = suc 𝑖 → (𝑓‘𝑎) = (𝑓‘suc 𝑖))
154		suceq 6437	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = suc 𝑖 → suc 𝑎 = suc suc 𝑖)
155	154	fveq2d 6900	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = suc 𝑖 → (𝑓‘suc 𝑎) = (𝑓‘suc suc 𝑖))
156	153, 155	breq12d 5162	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = suc 𝑖 → ((𝑓‘𝑎)𝑆(𝑓‘suc 𝑎) ↔ (𝑓‘suc 𝑖)𝑆(𝑓‘suc suc 𝑖)))
157	156	rspcv 3602	. . . . . . . . . . . . . . . . . . . 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 1230	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc suc 𝑖) = 𝑦)
160	158, 159	breqtrd 5175	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc 𝑖)𝑆𝑦)
161		breq1 5152	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = (𝑓‘suc 𝑖) → (𝑧𝑆𝑦 ↔ (𝑓‘suc 𝑖)𝑆𝑦))
162	101, 161	anbi12d 630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = (𝑓‘suc 𝑖) → ((𝑥𝑆𝑧 ∧ 𝑧𝑆𝑦) ↔ (𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦)))
163	96, 162	spcev 3590	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦) → ∃𝑧(𝑥𝑆𝑧 ∧ 𝑧𝑆𝑦))
164		vex 3465	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
165		vex 3465	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
166	164, 165	brco 5873	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥(𝑆 ∘ 𝑆)𝑦 ↔ ∃𝑧(𝑥𝑆𝑧 ∧ 𝑧𝑆𝑦))
167	163, 166	sylibr 233	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦) → 𝑥(𝑆 ∘ 𝑆)𝑦)
168		simplrr 776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑆 ∘ 𝑆) ⊆ 𝑆)
169	168	ssbrd 5192	. . . . . . . . . . . . . . . . . . 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 692	. . . . . . . . . . . . . . . . 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 1114	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)) → ((𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
177	176	exlimdv 1928	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)) → (∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
178	177	alrimiv 1922	. . . . . . . . . 10 ⊢ ((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
179	178	3exp 1116	. . . . . . . . 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 7904	. . . . . . 7 ⊢ (𝑛 ∈ ω → ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
182	181	com12 32	. . . . . 6 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → (𝑛 ∈ ω → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
183	182	ralrimiv 3134	. . . . 5 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑛 ∈ ω ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
184		ralcom4 3273	. . . . . 6 ⊢ (∀𝑛 ∈ ω ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦∀𝑛 ∈ ω (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
185		r19.23v 3172	. . . . . . 7 ⊢ (∀𝑛 ∈ ω (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
186	185	albii 1813	. . . . . 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 9739	. . . . . . 7 ⊢ (𝑥t++𝑅𝑦 ↔ ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
190		df-br 5150	. . . . . . 7 ⊢ (𝑥t++𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
191	189, 190	bitr3i 276	. . . . . 6 ⊢ (∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
192		df-br 5150	. . . . . 6 ⊢ (𝑥𝑆𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑆)
193	191, 192	imbi12i 349	. . . . 5 ⊢ ((∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
194	193	albii 1813	. . . 4 ⊢ (∀𝑦(∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
195	188, 194	sylib 217	. . 3 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
196	195	alrimiv 1922	. 2 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
197		relttrcl 9737	. . 3 ⊢ Rel t++𝑅
198		ssrel 5784	. . 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 1084 ∀wal 1531 = wceq 1533 ∃wex 1773 ∈ wcel 2098 ∀wral 3050 ∃wrex 3059 ⊆ wss 3944 ∅c0 4322 {csn 4630 ⟨cop 4636 class class class wbr 5149 ↾ cres 5680 ∘ ccom 5682 Rel wrel 5683 Ord word 6370 suc csuc 6373 Fn wfn 6544 ‘cfv 6549 ωcom 7871 1_oc1o 8480 t++cttrcl 9732

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 ax-un 7741

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2930 df-ral 3051 df-rex 3060 df-reu 3364 df-rab 3419 df-v 3463 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3964 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-int 4951 df-iun 4999 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-we 5635 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-pred 6307 df-ord 6374 df-on 6375 df-lim 6376 df-suc 6377 df-iota 6501 df-fun 6551 df-fn 6552 df-f 6553 df-f1 6554 df-fo 6555 df-f1o 6556 df-fv 6557 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7872 df-2nd 7995 df-frecs 8287 df-wrecs 8318 df-recs 8392 df-rdg 8431 df-1o 8487 df-oadd 8491 df-ttrcl 9733

This theorem is referenced by: dfttrcl2 9749

W3C validator