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 9610

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 6374	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → suc 𝑚 = suc ∅)
2		suceq 6374	. . . . . . . . . . . . . . 15 ⊢ (suc 𝑚 = suc ∅ → suc suc 𝑚 = suc suc ∅)
3	1, 2	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → suc suc 𝑚 = suc suc ∅)
4	3	fneq2d 6575	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc ∅))
5		df-1o 8385	. . . . . . . . . . . . . . . 16 ⊢ 1_o = suc ∅
6	1, 5	eqtr4di 2784	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → suc 𝑚 = 1_o)
7	6	fveqeq2d 6830	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘1_o) = 𝑦))
8	7	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦)))
9		df1o2 8392	. . . . . . . . . . . . . . . 16 ⊢ 1_o = {∅}
10	6, 9	eqtrdi 2782	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → suc 𝑚 = {∅})
11	10	raleqdv 3292	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ {∅} (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
12		0ex 5243	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ V
13		fveq2 6822	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∅ → (𝑓‘𝑎) = (𝑓‘∅))
14		suceq 6374	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = ∅ → suc 𝑎 = suc ∅)
15	14, 5	eqtr4di 2784	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∅ → suc 𝑎 = 1_o)
16	15	fveq2d 6826	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∅ → (𝑓‘suc 𝑎) = (𝑓‘1_o))
17	13, 16	breq12d 5102	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = ∅ → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∅)𝑅(𝑓‘1_o)))
18	12, 17	ralsn 4631	. . . . . . . . . . . . . 14 ⊢ (∀𝑎 ∈ {∅} (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∅)𝑅(𝑓‘1_o))
19	11, 18	bitrdi 287	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∅)𝑅(𝑓‘1_o)))
20	4, 8, 19	3anbi123d 1438	. . . . . . . . . . . 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 341	. . . . . . . . . 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 340	. . . . . . . 8 ⊢ (𝑚 = ∅ → (((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)) ↔ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑆𝑦))))
25		suceq 6374	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑖 → suc 𝑚 = suc 𝑖)
26		suceq 6374	. . . . . . . . . . . . . . . . 17 ⊢ (suc 𝑚 = suc 𝑖 → suc suc 𝑚 = suc suc 𝑖)
27	25, 26	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → suc suc 𝑚 = suc suc 𝑖)
28	27	fneq2d 6575	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc 𝑖))
29	25	fveqeq2d 6830	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘suc 𝑖) = 𝑦))
30	29	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦)))
31	25	raleqdv 3292	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
32		fveq2 6822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → (𝑓‘𝑎) = (𝑓‘𝑏))
33		suceq 6374	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑏 → suc 𝑎 = suc 𝑏)
34	33	fveq2d 6826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → (𝑓‘suc 𝑎) = (𝑓‘suc 𝑏))
35	32, 34	breq12d 5102	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘𝑏)𝑅(𝑓‘suc 𝑏)))
36	35	cbvralvw 3210	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑎 ∈ suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏))
37	31, 36	bitrdi 287	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏)))
38	28, 30, 37	3anbi123d 1438	. . . . . . . . . . . . . 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 6572	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (𝑓 Fn suc suc 𝑖 ↔ 𝑔 Fn suc suc 𝑖))
41		fveq1 6821	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘∅) = (𝑔‘∅))
42	41	eqeq1d 2733	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((𝑓‘∅) = 𝑥 ↔ (𝑔‘∅) = 𝑥))
43		fveq1 6821	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘suc 𝑖) = (𝑔‘suc 𝑖))
44	43	eqeq1d 2733	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((𝑓‘suc 𝑖) = 𝑦 ↔ (𝑔‘suc 𝑖) = 𝑦))
45	42, 44	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ↔ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦)))
46		fveq1 6821	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑏) = (𝑔‘𝑏))
47		fveq1 6821	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘suc 𝑏) = (𝑔‘suc 𝑏))
48	46, 47	breq12d 5102	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑏)𝑅(𝑓‘suc 𝑏) ↔ (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
49	48	ralbidv 3155	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏) ↔ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
50	40, 45, 49	3anbi123d 1438	. . . . . . . . . . . . . 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 287	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑖 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
53	52	imbi1d 341	. . . . . . . . . . 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 2743	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → ((𝑔‘suc 𝑖) = 𝑦 ↔ (𝑔‘suc 𝑖) = 𝑧))
56	55	anbi2d 630	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → (((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ↔ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧)))
57	56	3anbi2d 1443	. . . . . . . . . . . . 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 5093	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑥𝑆𝑦 ↔ 𝑥𝑆𝑧))
60	58, 59	imbi12d 344	. . . . . . . . . . 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 287	. . . . . . . . 9 ⊢ (𝑚 = 𝑖 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)))
63	62	imbi2d 340	. . . . . . . 8 ⊢ (𝑚 = 𝑖 → (((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)) ↔ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧))))
64		suceq 6374	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = suc 𝑖 → suc 𝑚 = suc suc 𝑖)
65		suceq 6374	. . . . . . . . . . . . . . 15 ⊢ (suc 𝑚 = suc suc 𝑖 → suc suc 𝑚 = suc suc suc 𝑖)
66	64, 65	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑚 = suc 𝑖 → suc suc 𝑚 = suc suc suc 𝑖)
67	66	fneq2d 6575	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc suc 𝑖))
68	64	fveqeq2d 6830	. . . . . . . . . . . . . 14 ⊢ (𝑚 = suc 𝑖 → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘suc suc 𝑖) = 𝑦))
69	68	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦)))
70	64	raleqdv 3292	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
71	67, 69, 70	3anbi123d 1438	. . . . . . . . . . . 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 341	. . . . . . . . . 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 340	. . . . . . . 8 ⊢ (𝑚 = suc 𝑖 → (((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)) ↔ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))))
76		suceq 6374	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑛 → suc 𝑚 = suc 𝑛)
77		suceq 6374	. . . . . . . . . . . . . . 15 ⊢ (suc 𝑚 = suc 𝑛 → suc suc 𝑚 = suc suc 𝑛)
78	76, 77	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → suc suc 𝑚 = suc suc 𝑛)
79	78	fneq2d 6575	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc 𝑛))
80	76	fveqeq2d 6830	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘suc 𝑛) = 𝑦))
81	80	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦)))
82	76	raleqdv 3292	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
83	79, 81, 82	3anbi123d 1438	. . . . . . . . . . . 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 341	. . . . . . . . . 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 340	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)) ↔ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))))
88		breq12 5094	. . . . . . . . . . . . 13 ⊢ (((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) → ((𝑓‘∅)𝑅(𝑓‘1_o) ↔ 𝑥𝑅𝑦))
89	88	biimpa 476	. . . . . . . . . . . 12 ⊢ ((((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑅𝑦)
90	89	3adant1 1130	. . . . . . . . . . 11 ⊢ ((𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑅𝑦)
91		ssbr 5133	. . . . . . . . . . . 12 ⊢ (𝑅 ⊆ 𝑆 → (𝑥𝑅𝑦 → 𝑥𝑆𝑦))
92	91	adantr 480	. . . . . . . . . . 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 6835	. . . . . . . . . . . . . . 15 ⊢ (𝑓‘suc 𝑖) ∈ V
97		eqeq2 2743	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘suc 𝑖) → ((𝑔‘suc 𝑖) = 𝑧 ↔ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)))
98	97	anbi2d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑓‘suc 𝑖) → (((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ↔ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖))))
99	98	3anbi2d 1443	. . . . . . . . . . . . . . . . 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 5093	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑓‘suc 𝑖) → (𝑥𝑆𝑧 ↔ 𝑥𝑆(𝑓‘suc 𝑖)))
102	100, 101	imbi12d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑓‘suc 𝑖) → ((∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧) ↔ (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆(𝑓‘suc 𝑖))))
103	96, 102	spcv 3555	. . . . . . . . . . . . . 14 ⊢ (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧) → (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆(𝑓‘suc 𝑖)))
104		simpr1 1195	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → 𝑓 Fn suc suc suc 𝑖)
105		sssucid 6388	. . . . . . . . . . . . . . . . . . 19 ⊢ suc suc 𝑖 ⊆ suc suc suc 𝑖
106		fnssres 6604	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 Fn suc suc suc 𝑖 ∧ suc suc 𝑖 ⊆ suc suc suc 𝑖) → (𝑓 ↾ suc suc 𝑖) Fn suc suc 𝑖)
107	104, 105, 106	sylancl 586	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓 ↾ suc suc 𝑖) Fn suc suc 𝑖)
108		peano2 7820	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ ω → suc 𝑖 ∈ ω)
109	108	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → suc 𝑖 ∈ ω)
110		nnord 7804	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc 𝑖 ∈ ω → Ord suc 𝑖)
111	109, 110	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → Ord suc 𝑖)
112		0elsuc 7765	. . . . . . . . . . . . . . . . . . . . 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 6842	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ((𝑓 ↾ suc suc 𝑖)‘∅) = (𝑓‘∅))
115		simpr2l 1233	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∅) = 𝑥)
116	114, 115	eqtrd 2766	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥)
117		vex 3440	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑖 ∈ V
118	117	sucex 7739	. . . . . . . . . . . . . . . . . . . 20 ⊢ suc 𝑖 ∈ V
119	118	sucid 6390	. . . . . . . . . . . . . . . . . . 19 ⊢ suc 𝑖 ∈ suc suc 𝑖
120		fvres 6841	. . . . . . . . . . . . . . . . . . 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 1218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))
123		elelsuc 6381	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 ∈ suc 𝑖 → 𝑏 ∈ suc suc 𝑖)
124	123	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → 𝑏 ∈ suc suc 𝑖)
125	35, 122, 124	rspcdva 3573	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → (𝑓‘𝑏)𝑅(𝑓‘suc 𝑏))
126	124	fvresd 6842	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ((𝑓 ↾ suc suc 𝑖)‘𝑏) = (𝑓‘𝑏))
127		ordsucelsuc 7752	. . . . . . . . . . . . . . . . . . . . . . 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 476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → suc 𝑏 ∈ suc suc 𝑖)
130	129	fvresd 6842	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ((𝑓 ↾ suc suc 𝑖)‘suc 𝑏) = (𝑓‘suc 𝑏))
131	125, 126, 130	3brtr4d 5121	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏))
132	131	ralrimiva 3124	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑏 ∈ suc 𝑖((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏))
133		vex 3440	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑓 ∈ V
134	133	resex 5977	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ↾ suc suc 𝑖) ∈ V
135		fneq1 6572	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔 Fn suc suc 𝑖 ↔ (𝑓 ↾ suc suc 𝑖) Fn suc suc 𝑖))
136		fveq1 6821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘∅) = ((𝑓 ↾ suc suc 𝑖)‘∅))
137	136	eqeq1d 2733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → ((𝑔‘∅) = 𝑥 ↔ ((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥))
138		fveq1 6821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘suc 𝑖) = ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖))
139	138	eqeq1d 2733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → ((𝑔‘suc 𝑖) = (𝑓‘suc 𝑖) ↔ ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖) = (𝑓‘suc 𝑖)))
140	137, 139	anbi12d 632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ↔ (((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥 ∧ ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖) = (𝑓‘suc 𝑖))))
141		fveq1 6821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘𝑏) = ((𝑓 ↾ suc suc 𝑖)‘𝑏))
142		fveq1 6821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘suc 𝑏) = ((𝑓 ↾ suc suc 𝑖)‘suc 𝑏))
143	141, 142	breq12d 5102	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → ((𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ ((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏)))
144	143	ralbidv 3155	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ ∀𝑏 ∈ suc 𝑖((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏)))
145	135, 140, 144	3anbi123d 1438	. . . . . . . . . . . . . . . . . . 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 3556	. . . . . . . . . . . . . . . . . 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 1377	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
148		simplrl 776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → 𝑅 ⊆ 𝑆)
149		simpr3 1197	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))
150		ssbr 5133	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ⊆ 𝑆 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) → (𝑓‘𝑎)𝑆(𝑓‘suc 𝑎)))
151	150	ralimdv 3146	. . . . . . . . . . . . . . . . . . . . 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 6822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = suc 𝑖 → (𝑓‘𝑎) = (𝑓‘suc 𝑖))
154		suceq 6374	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = suc 𝑖 → suc 𝑎 = suc suc 𝑖)
155	154	fveq2d 6826	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = suc 𝑖 → (𝑓‘suc 𝑎) = (𝑓‘suc suc 𝑖))
156	153, 155	breq12d 5102	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = suc 𝑖 → ((𝑓‘𝑎)𝑆(𝑓‘suc 𝑎) ↔ (𝑓‘suc 𝑖)𝑆(𝑓‘suc suc 𝑖)))
157	156	rspcv 3568	. . . . . . . . . . . . . . . . . . . 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 1234	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc suc 𝑖) = 𝑦)
160	158, 159	breqtrd 5115	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc 𝑖)𝑆𝑦)
161		breq1 5092	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = (𝑓‘suc 𝑖) → (𝑧𝑆𝑦 ↔ (𝑓‘suc 𝑖)𝑆𝑦))
162	101, 161	anbi12d 632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = (𝑓‘suc 𝑖) → ((𝑥𝑆𝑧 ∧ 𝑧𝑆𝑦) ↔ (𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦)))
163	96, 162	spcev 3556	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦) → ∃𝑧(𝑥𝑆𝑧 ∧ 𝑧𝑆𝑦))
164		vex 3440	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
165		vex 3440	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
166	164, 165	brco 5809	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥(𝑆 ∘ 𝑆)𝑦 ↔ ∃𝑧(𝑥𝑆𝑧 ∧ 𝑧𝑆𝑦))
167	163, 166	sylibr 234	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦) → 𝑥(𝑆 ∘ 𝑆)𝑦)
168		simplrr 777	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑆 ∘ 𝑆) ⊆ 𝑆)
169	168	ssbrd 5132	. . . . . . . . . . . . . . . . . . 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 694	. . . . . . . . . . . . . . . . 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 412	. . . . . . . . . . . . . . 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 1117	. . . . . . . . . . . 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 1119	. . . . . . . . 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 7826	. . . . . . 7 ⊢ (𝑛 ∈ ω → ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
182	181	com12 32	. . . . . 6 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → (𝑛 ∈ ω → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
183	182	ralrimiv 3123	. . . . 5 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑛 ∈ ω ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
184		ralcom4 3258	. . . . . 6 ⊢ (∀𝑛 ∈ ω ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦∀𝑛 ∈ ω (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
185		r19.23v 3159	. . . . . . 7 ⊢ (∀𝑛 ∈ ω (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
186	185	albii 1820	. . . . . 6 ⊢ (∀𝑦∀𝑛 ∈ ω (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
187	184, 186	bitri 275	. . . . 5 ⊢ (∀𝑛 ∈ ω ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
188	183, 187	sylib 218	. . . 4 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
189		brttrcl2 9604	. . . . . . 7 ⊢ (𝑥t++𝑅𝑦 ↔ ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
190		df-br 5090	. . . . . . 7 ⊢ (𝑥t++𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
191	189, 190	bitr3i 277	. . . . . 6 ⊢ (∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
192		df-br 5090	. . . . . 6 ⊢ (𝑥𝑆𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑆)
193	191, 192	imbi12i 350	. . . . 5 ⊢ ((∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
194	193	albii 1820	. . . 4 ⊢ (∀𝑦(∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
195	188, 194	sylib 218	. . 3 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
196	195	alrimiv 1928	. 2 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
197		relttrcl 9602	. . 3 ⊢ Rel t++𝑅
198		ssrel 5722	. . 3 ⊢ (Rel t++𝑅 → (t++𝑅 ⊆ 𝑆 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆)))
199	197, 198	ax-mp 5	. 2 ⊢ (t++𝑅 ⊆ 𝑆 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
200	196, 199	sylibr 234	1 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → t++𝑅 ⊆ 𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 ∀wal 1539 = wceq 1541 ∃wex 1780 ∈ wcel 2111 ∀wral 3047 ∃wrex 3056 ⊆ wss 3897 ∅c0 4280 {csn 4573 ⟨cop 4579 class class class wbr 5089 ↾ cres 5616 ∘ ccom 5618 Rel wrel 5619 Ord word 6305 suc csuc 6308 Fn wfn 6476 ‘cfv 6481 ωcom 7796 1_oc1o 8378 t++cttrcl 9597

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5232 ax-nul 5242 ax-pr 5368 ax-un 7668

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-ral 3048 df-rex 3057 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-int 4896 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-oadd 8389 df-ttrcl 9598

This theorem is referenced by: dfttrcl2 9614

W3C validator