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 9758

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 6452	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → suc 𝑚 = suc ∅)
2		suceq 6452	. . . . . . . . . . . . . . 15 ⊢ (suc 𝑚 = suc ∅ → suc suc 𝑚 = suc suc ∅)
3	1, 2	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → suc suc 𝑚 = suc suc ∅)
4	3	fneq2d 6663	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc ∅))
5		df-1o 8505	. . . . . . . . . . . . . . . 16 ⊢ 1_o = suc ∅
6	1, 5	eqtr4di 2793	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → suc 𝑚 = 1_o)
7	6	fveqeq2d 6915	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘1_o) = 𝑦))
8	7	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦)))
9		df1o2 8512	. . . . . . . . . . . . . . . 16 ⊢ 1_o = {∅}
10	6, 9	eqtrdi 2791	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → suc 𝑚 = {∅})
11	10	raleqdv 3324	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ {∅} (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
12		0ex 5313	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ V
13		fveq2 6907	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∅ → (𝑓‘𝑎) = (𝑓‘∅))
14		suceq 6452	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = ∅ → suc 𝑎 = suc ∅)
15	14, 5	eqtr4di 2793	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∅ → suc 𝑎 = 1_o)
16	15	fveq2d 6911	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∅ → (𝑓‘suc 𝑎) = (𝑓‘1_o))
17	13, 16	breq12d 5161	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = ∅ → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∅)𝑅(𝑓‘1_o)))
18	12, 17	ralsn 4686	. . . . . . . . . . . . . 14 ⊢ (∀𝑎 ∈ {∅} (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∅)𝑅(𝑓‘1_o))
19	11, 18	bitrdi 287	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∅)𝑅(𝑓‘1_o)))
20	4, 8, 19	3anbi123d 1435	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o))))
21	20	exbidv 1919	. . . . . . . . . . 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 1918	. . . . . . . . 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 6452	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑖 → suc 𝑚 = suc 𝑖)
26		suceq 6452	. . . . . . . . . . . . . . . . 17 ⊢ (suc 𝑚 = suc 𝑖 → suc suc 𝑚 = suc suc 𝑖)
27	25, 26	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → suc suc 𝑚 = suc suc 𝑖)
28	27	fneq2d 6663	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc 𝑖))
29	25	fveqeq2d 6915	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘suc 𝑖) = 𝑦))
30	29	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦)))
31	25	raleqdv 3324	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
32		fveq2 6907	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → (𝑓‘𝑎) = (𝑓‘𝑏))
33		suceq 6452	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑏 → suc 𝑎 = suc 𝑏)
34	33	fveq2d 6911	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → (𝑓‘suc 𝑎) = (𝑓‘suc 𝑏))
35	32, 34	breq12d 5161	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘𝑏)𝑅(𝑓‘suc 𝑏)))
36	35	cbvralvw 3235	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑎 ∈ suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏))
37	31, 36	bitrdi 287	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏)))
38	28, 30, 37	3anbi123d 1435	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑖 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏))))
39	38	exbidv 1919	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏))))
40		fneq1 6660	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (𝑓 Fn suc suc 𝑖 ↔ 𝑔 Fn suc suc 𝑖))
41		fveq1 6906	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘∅) = (𝑔‘∅))
42	41	eqeq1d 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((𝑓‘∅) = 𝑥 ↔ (𝑔‘∅) = 𝑥))
43		fveq1 6906	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘suc 𝑖) = (𝑔‘suc 𝑖))
44	43	eqeq1d 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((𝑓‘suc 𝑖) = 𝑦 ↔ (𝑔‘suc 𝑖) = 𝑦))
45	42, 44	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ↔ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦)))
46		fveq1 6906	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑏) = (𝑔‘𝑏))
47		fveq1 6906	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘suc 𝑏) = (𝑔‘suc 𝑏))
48	46, 47	breq12d 5161	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑏)𝑅(𝑓‘suc 𝑏) ↔ (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
49	48	ralbidv 3176	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏) ↔ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
50	40, 45, 49	3anbi123d 1435	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → ((𝑓 Fn suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏)) ↔ (𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
51	50	cbvexvw 2034	. . . . . . . . . . . . 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 1918	. . . . . . . . . 10 ⊢ (𝑚 = 𝑖 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑦)))
55		eqeq2 2747	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → ((𝑔‘suc 𝑖) = 𝑦 ↔ (𝑔‘suc 𝑖) = 𝑧))
56	55	anbi2d 630	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → (((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ↔ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧)))
57	56	3anbi2d 1440	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → ((𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) ↔ (𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
58	57	exbidv 1919	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
59		breq2 5152	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑥𝑆𝑦 ↔ 𝑥𝑆𝑧))
60	58, 59	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑦) ↔ (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)))
61	60	cbvalvw 2033	. . . . . . . . . 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 6452	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = suc 𝑖 → suc 𝑚 = suc suc 𝑖)
65		suceq 6452	. . . . . . . . . . . . . . 15 ⊢ (suc 𝑚 = suc suc 𝑖 → suc suc 𝑚 = suc suc suc 𝑖)
66	64, 65	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑚 = suc 𝑖 → suc suc 𝑚 = suc suc suc 𝑖)
67	66	fneq2d 6663	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc suc 𝑖))
68	64	fveqeq2d 6915	. . . . . . . . . . . . . 14 ⊢ (𝑚 = suc 𝑖 → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘suc suc 𝑖) = 𝑦))
69	68	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦)))
70	64	raleqdv 3324	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
71	67, 69, 70	3anbi123d 1435	. . . . . . . . . . . 12 ⊢ (𝑚 = suc 𝑖 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
72	71	exbidv 1919	. . . . . . . . . . 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 1918	. . . . . . . . 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 6452	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑛 → suc 𝑚 = suc 𝑛)
77		suceq 6452	. . . . . . . . . . . . . . 15 ⊢ (suc 𝑚 = suc 𝑛 → suc suc 𝑚 = suc suc 𝑛)
78	76, 77	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → suc suc 𝑚 = suc suc 𝑛)
79	78	fneq2d 6663	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc 𝑛))
80	76	fveqeq2d 6915	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘suc 𝑛) = 𝑦))
81	80	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦)))
82	76	raleqdv 3324	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
83	79, 81, 82	3anbi123d 1435	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
84	83	exbidv 1919	. . . . . . . . . . 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 1918	. . . . . . . . 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 5153	. . . . . . . . . . . . 13 ⊢ (((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) → ((𝑓‘∅)𝑅(𝑓‘1_o) ↔ 𝑥𝑅𝑦))
89	88	biimpa 476	. . . . . . . . . . . 12 ⊢ ((((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑅𝑦)
90	89	3adant1 1129	. . . . . . . . . . 11 ⊢ ((𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑅𝑦)
91		ssbr 5192	. . . . . . . . . . . 12 ⊢ (𝑅 ⊆ 𝑆 → (𝑥𝑅𝑦 → 𝑥𝑆𝑦))
92	91	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → (𝑥𝑅𝑦 → 𝑥𝑆𝑦))
93	90, 92	syl5 34	. . . . . . . . . 10 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ((𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑆𝑦))
94	93	exlimdv 1931	. . . . . . . . 9 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → (∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑆𝑦))
95	94	alrimiv 1925	. . . . . . . 8 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑆𝑦))
96		fvex 6920	. . . . . . . . . . . . . . 15 ⊢ (𝑓‘suc 𝑖) ∈ V
97		eqeq2 2747	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘suc 𝑖) → ((𝑔‘suc 𝑖) = 𝑧 ↔ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)))
98	97	anbi2d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑓‘suc 𝑖) → (((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ↔ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖))))
99	98	3anbi2d 1440	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑓‘suc 𝑖) → ((𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) ↔ (𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
100	99	exbidv 1919	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑓‘suc 𝑖) → (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
101		breq2 5152	. . . . . . . . . . . . . . . 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 3605	. . . . . . . . . . . . . 14 ⊢ (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧) → (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆(𝑓‘suc 𝑖)))
104		simpr1 1193	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → 𝑓 Fn suc suc suc 𝑖)
105		sssucid 6466	. . . . . . . . . . . . . . . . . . 19 ⊢ suc suc 𝑖 ⊆ suc suc suc 𝑖
106		fnssres 6692	. . . . . . . . . . . . . . . . . . 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 7913	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ ω → suc 𝑖 ∈ ω)
109	108	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → suc 𝑖 ∈ ω)
110		nnord 7895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc 𝑖 ∈ ω → Ord suc 𝑖)
111	109, 110	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → Ord suc 𝑖)
112		0elsuc 7855	. . . . . . . . . . . . . . . . . . . . 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 6927	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ((𝑓 ↾ suc suc 𝑖)‘∅) = (𝑓‘∅))
115		simpr2l 1231	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∅) = 𝑥)
116	114, 115	eqtrd 2775	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥)
117		vex 3482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑖 ∈ V
118	117	sucex 7826	. . . . . . . . . . . . . . . . . . . 20 ⊢ suc 𝑖 ∈ V
119	118	sucid 6468	. . . . . . . . . . . . . . . . . . 19 ⊢ suc 𝑖 ∈ suc suc 𝑖
120		fvres 6926	. . . . . . . . . . . . . . . . . . 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 1216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))
123		elelsuc 6459	. . . . . . . . . . . . . . . . . . . . . 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 3623	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → (𝑓‘𝑏)𝑅(𝑓‘suc 𝑏))
126	124	fvresd 6927	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ((𝑓 ↾ suc suc 𝑖)‘𝑏) = (𝑓‘𝑏))
127		ordsucelsuc 7842	. . . . . . . . . . . . . . . . . . . . . . 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 6927	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ((𝑓 ↾ suc suc 𝑖)‘suc 𝑏) = (𝑓‘suc 𝑏))
131	125, 126, 130	3brtr4d 5180	. . . . . . . . . . . . . . . . . . 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 3482	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑓 ∈ V
134	133	resex 6049	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ↾ suc suc 𝑖) ∈ V
135		fneq1 6660	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔 Fn suc suc 𝑖 ↔ (𝑓 ↾ suc suc 𝑖) Fn suc suc 𝑖))
136		fveq1 6906	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘∅) = ((𝑓 ↾ suc suc 𝑖)‘∅))
137	136	eqeq1d 2737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → ((𝑔‘∅) = 𝑥 ↔ ((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥))
138		fveq1 6906	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘suc 𝑖) = ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖))
139	138	eqeq1d 2737	. . . . . . . . . . . . . . . . . . . . 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 6906	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘𝑏) = ((𝑓 ↾ suc suc 𝑖)‘𝑏))
142		fveq1 6906	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘suc 𝑏) = ((𝑓 ↾ suc suc 𝑖)‘suc 𝑏))
143	141, 142	breq12d 5161	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → ((𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ ((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏)))
144	143	ralbidv 3176	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ ∀𝑏 ∈ suc 𝑖((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏)))
145	135, 140, 144	3anbi123d 1435	. . . . . . . . . . . . . . . . . . 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 3606	. . . . . . . . . . . . . . . . . 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 1374	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
148		simplrl 777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → 𝑅 ⊆ 𝑆)
149		simpr3 1195	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))
150		ssbr 5192	. . . . . . . . . . . . . . . . . . . . . 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 6907	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = suc 𝑖 → (𝑓‘𝑎) = (𝑓‘suc 𝑖))
154		suceq 6452	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = suc 𝑖 → suc 𝑎 = suc suc 𝑖)
155	154	fveq2d 6911	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = suc 𝑖 → (𝑓‘suc 𝑎) = (𝑓‘suc suc 𝑖))
156	153, 155	breq12d 5161	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = suc 𝑖 → ((𝑓‘𝑎)𝑆(𝑓‘suc 𝑎) ↔ (𝑓‘suc 𝑖)𝑆(𝑓‘suc suc 𝑖)))
157	156	rspcv 3618	. . . . . . . . . . . . . . . . . . . 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 1232	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc suc 𝑖) = 𝑦)
160	158, 159	breqtrd 5174	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc 𝑖)𝑆𝑦)
161		breq1 5151	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = (𝑓‘suc 𝑖) → (𝑧𝑆𝑦 ↔ (𝑓‘suc 𝑖)𝑆𝑦))
162	101, 161	anbi12d 632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = (𝑓‘suc 𝑖) → ((𝑥𝑆𝑧 ∧ 𝑧𝑆𝑦) ↔ (𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦)))
163	96, 162	spcev 3606	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦) → ∃𝑧(𝑥𝑆𝑧 ∧ 𝑧𝑆𝑦))
164		vex 3482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
165		vex 3482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
166	164, 165	brco 5884	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥(𝑆 ∘ 𝑆)𝑦 ↔ ∃𝑧(𝑥𝑆𝑧 ∧ 𝑧𝑆𝑦))
167	163, 166	sylibr 234	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦) → 𝑥(𝑆 ∘ 𝑆)𝑦)
168		simplrr 778	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑆 ∘ 𝑆) ⊆ 𝑆)
169	168	ssbrd 5191	. . . . . . . . . . . . . . . . . . 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 1116	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)) → ((𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
177	176	exlimdv 1931	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)) → (∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
178	177	alrimiv 1925	. . . . . . . . . 10 ⊢ ((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
179	178	3exp 1118	. . . . . . . . 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 7919	. . . . . . 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 3284	. . . . . 6 ⊢ (∀𝑛 ∈ ω ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦∀𝑛 ∈ ω (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
185		r19.23v 3181	. . . . . . 7 ⊢ (∀𝑛 ∈ ω (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
186	185	albii 1816	. . . . . 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 9752	. . . . . . 7 ⊢ (𝑥t++𝑅𝑦 ↔ ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
190		df-br 5149	. . . . . . 7 ⊢ (𝑥t++𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
191	189, 190	bitr3i 277	. . . . . 6 ⊢ (∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
192		df-br 5149	. . . . . 6 ⊢ (𝑥𝑆𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑆)
193	191, 192	imbi12i 350	. . . . 5 ⊢ ((∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
194	193	albii 1816	. . . 4 ⊢ (∀𝑦(∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
195	188, 194	sylib 218	. . 3 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
196	195	alrimiv 1925	. 2 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
197		relttrcl 9750	. . 3 ⊢ Rel t++𝑅
198		ssrel 5795	. . 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 1535 = wceq 1537 ∃wex 1776 ∈ wcel 2106 ∀wral 3059 ∃wrex 3068 ⊆ wss 3963 ∅c0 4339 {csn 4631 ⟨cop 4637 class class class wbr 5148 ↾ cres 5691 ∘ ccom 5693 Rel wrel 5694 Ord word 6385 suc csuc 6388 Fn wfn 6558 ‘cfv 6563 ωcom 7887 1_oc1o 8498 t++cttrcl 9745

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pr 5438 ax-un 7754

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-ral 3060 df-rex 3069 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-int 4952 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-2nd 8014 df-frecs 8305 df-wrecs 8336 df-recs 8410 df-rdg 8449 df-1o 8505 df-oadd 8509 df-ttrcl 9746

This theorem is referenced by: dfttrcl2 9762

W3C validator