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 9734

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 6438	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → suc 𝑚 = suc ∅)
2		suceq 6438	. . . . . . . . . . . . . . 15 ⊢ (suc 𝑚 = suc ∅ → suc suc 𝑚 = suc suc ∅)
3	1, 2	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → suc suc 𝑚 = suc suc ∅)
4	3	fneq2d 6644	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc ∅))
5		df-1o 8490	. . . . . . . . . . . . . . . 16 ⊢ 1_o = suc ∅
6	1, 5	eqtr4di 2816	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → suc 𝑚 = 1_o)
7	6	fveqeq2d 6904	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘1_o) = 𝑦))
8	7	anbi2d 642	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦)))
9		df1o2 8497	. . . . . . . . . . . . . . . 16 ⊢ 1_o = {∅}
10	6, 9	eqtrdi 2814	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → suc 𝑚 = {∅})
11	10	raleqdv 3323	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ {∅} (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
12		0ex 5264	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ V
13		fveq2 6896	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∅ → (𝑓‘𝑎) = (𝑓‘∅))
14		suceq 6438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = ∅ → suc 𝑎 = suc ∅)
15	14, 5	eqtr4di 2816	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∅ → suc 𝑎 = 1_o)
16	15	fveq2d 6900	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∅ → (𝑓‘suc 𝑎) = (𝑓‘1_o))
17	13, 16	breq12d 5119	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = ∅ → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∅)𝑅(𝑓‘1_o)))
18	12, 17	ralsn 4642	. . . . . . . . . . . . . 14 ⊢ (∀𝑎 ∈ {∅} (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∅)𝑅(𝑓‘1_o))
19	11, 18	bitrdi 290	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘∅)𝑅(𝑓‘1_o)))
20	4, 8, 19	3anbi123d 1464	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o))))
21	20	exbidv 1955	. . . . . . . . . . 11 ⊢ (𝑚 = ∅ → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o))))
22	21	imbi1d 344	. . . . . . . . . 10 ⊢ (𝑚 = ∅ → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑆𝑦)))
23	22	albidv 1954	. . . . . . . . 9 ⊢ (𝑚 = ∅ → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑆𝑦)))
24	23	imbi2d 343	. . . . . . . 8 ⊢ (𝑚 = ∅ → (((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)) ↔ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑆𝑦))))
25		suceq 6438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑖 → suc 𝑚 = suc 𝑖)
26		suceq 6438	. . . . . . . . . . . . . . . . 17 ⊢ (suc 𝑚 = suc 𝑖 → suc suc 𝑚 = suc suc 𝑖)
27	25, 26	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → suc suc 𝑚 = suc suc 𝑖)
28	27	fneq2d 6644	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc 𝑖))
29	25	fveqeq2d 6904	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘suc 𝑖) = 𝑦))
30	29	anbi2d 642	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦)))
31	25	raleqdv 3323	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
32		fveq2 6896	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → (𝑓‘𝑎) = (𝑓‘𝑏))
33		suceq 6438	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑏 → suc 𝑎 = suc 𝑏)
34	33	fveq2d 6900	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → (𝑓‘suc 𝑎) = (𝑓‘suc 𝑏))
35	32, 34	breq12d 5119	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ (𝑓‘𝑏)𝑅(𝑓‘suc 𝑏)))
36	35	cbvralvw 3244	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑎 ∈ suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏))
37	31, 36	bitrdi 290	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏)))
38	28, 30, 37	3anbi123d 1464	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑖 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏))))
39	38	exbidv 1955	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏))))
40		fneq1 6641	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (𝑓 Fn suc suc 𝑖 ↔ 𝑔 Fn suc suc 𝑖))
41		fveq1 6895	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘∅) = (𝑔‘∅))
42	41	eqeq1d 2765	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((𝑓‘∅) = 𝑥 ↔ (𝑔‘∅) = 𝑥))
43		fveq1 6895	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘suc 𝑖) = (𝑔‘suc 𝑖))
44	43	eqeq1d 2765	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((𝑓‘suc 𝑖) = 𝑦 ↔ (𝑔‘suc 𝑖) = 𝑦))
45	42, 44	anbi12d 644	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ↔ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦)))
46		fveq1 6895	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑏) = (𝑔‘𝑏))
47		fveq1 6895	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘suc 𝑏) = (𝑔‘suc 𝑏))
48	46, 47	breq12d 5119	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑏)𝑅(𝑓‘suc 𝑏) ↔ (𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
49	48	ralbidv 3189	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏) ↔ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
50	40, 45, 49	3anbi123d 1464	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → ((𝑓 Fn suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏)) ↔ (𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
51	50	cbvexvw 2071	. . . . . . . . . . . . 13 ⊢ (∃𝑓(𝑓 Fn suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑓‘𝑏)𝑅(𝑓‘suc 𝑏)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
52	39, 51	bitrdi 290	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑖 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
53	52	imbi1d 344	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑖 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑦)))
54	53	albidv 1954	. . . . . . . . . 10 ⊢ (𝑚 = 𝑖 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑦)))
55		eqeq2 2775	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → ((𝑔‘suc 𝑖) = 𝑦 ↔ (𝑔‘suc 𝑖) = 𝑧))
56	55	anbi2d 642	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → (((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ↔ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧)))
57	56	3anbi2d 1469	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → ((𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) ↔ (𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
58	57	exbidv 1955	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
59		breq2 5110	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑥𝑆𝑦 ↔ 𝑥𝑆𝑧))
60	58, 59	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑦) ↔ (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)))
61	60	cbvalvw 2070	. . . . . . . . . 10 ⊢ (∀𝑦(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑦) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑦) ↔ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧))
62	54, 61	bitrdi 290	. . . . . . . . 9 ⊢ (𝑚 = 𝑖 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)))
63	62	imbi2d 343	. . . . . . . 8 ⊢ (𝑚 = 𝑖 → (((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)) ↔ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧))))
64		suceq 6438	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = suc 𝑖 → suc 𝑚 = suc suc 𝑖)
65		suceq 6438	. . . . . . . . . . . . . . 15 ⊢ (suc 𝑚 = suc suc 𝑖 → suc suc 𝑚 = suc suc suc 𝑖)
66	64, 65	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑚 = suc 𝑖 → suc suc 𝑚 = suc suc suc 𝑖)
67	66	fneq2d 6644	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc suc 𝑖))
68	64	fveqeq2d 6904	. . . . . . . . . . . . . 14 ⊢ (𝑚 = suc 𝑖 → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘suc suc 𝑖) = 𝑦))
69	68	anbi2d 642	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦)))
70	64	raleqdv 3323	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
71	67, 69, 70	3anbi123d 1464	. . . . . . . . . . . 12 ⊢ (𝑚 = suc 𝑖 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
72	71	exbidv 1955	. . . . . . . . . . 11 ⊢ (𝑚 = suc 𝑖 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
73	72	imbi1d 344	. . . . . . . . . 10 ⊢ (𝑚 = suc 𝑖 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
74	73	albidv 1954	. . . . . . . . 9 ⊢ (𝑚 = suc 𝑖 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
75	74	imbi2d 343	. . . . . . . 8 ⊢ (𝑚 = suc 𝑖 → (((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)) ↔ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))))
76		suceq 6438	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑛 → suc 𝑚 = suc 𝑛)
77		suceq 6438	. . . . . . . . . . . . . . 15 ⊢ (suc 𝑚 = suc 𝑛 → suc suc 𝑚 = suc suc 𝑛)
78	76, 77	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → suc suc 𝑚 = suc suc 𝑛)
79	78	fneq2d 6644	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc 𝑛))
80	76	fveqeq2d 6904	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → ((𝑓‘suc 𝑚) = 𝑦 ↔ (𝑓‘suc 𝑛) = 𝑦))
81	80	anbi2d 642	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦)))
82	76	raleqdv 3323	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
83	79, 81, 82	3anbi123d 1464	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
84	83	exbidv 1955	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
85	84	imbi1d 344	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
86	85	albidv 1954	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
87	86	imbi2d 343	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑚) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)) ↔ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))))
88		breq12 5111	. . . . . . . . . . . . 13 ⊢ (((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) → ((𝑓‘∅)𝑅(𝑓‘1_o) ↔ 𝑥𝑅𝑦))
89	88	biimpa 482	. . . . . . . . . . . 12 ⊢ ((((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑅𝑦)
90	89	3adant1 1148	. . . . . . . . . . 11 ⊢ ((𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑅𝑦)
91		ssbr 5152	. . . . . . . . . . . 12 ⊢ (𝑅 ⊆ 𝑆 → (𝑥𝑅𝑦 → 𝑥𝑆𝑦))
92	91	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → (𝑥𝑅𝑦 → 𝑥𝑆𝑦))
93	90, 92	syl5 35	. . . . . . . . . 10 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ((𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑆𝑦))
94	93	exlimdv 1967	. . . . . . . . 9 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → (∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑆𝑦))
95	94	alrimiv 1961	. . . . . . . 8 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc ∅ ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1_o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1_o)) → 𝑥𝑆𝑦))
96		fvex 6909	. . . . . . . . . . . . . . 15 ⊢ (𝑓‘suc 𝑖) ∈ V
97		eqeq2 2775	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘suc 𝑖) → ((𝑔‘suc 𝑖) = 𝑧 ↔ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)))
98	97	anbi2d 642	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑓‘suc 𝑖) → (((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ↔ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖))))
99	98	3anbi2d 1469	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑓‘suc 𝑖) → ((𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) ↔ (𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
100	99	exbidv 1955	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑓‘suc 𝑖) → (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏))))
101		breq2 5110	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑓‘suc 𝑖) → (𝑥𝑆𝑧 ↔ 𝑥𝑆(𝑓‘suc 𝑖)))
102	100, 101	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑓‘suc 𝑖) → ((∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧) ↔ (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆(𝑓‘suc 𝑖))))
103	96, 102	spcv 3563	. . . . . . . . . . . . . 14 ⊢ (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧) → (∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆(𝑓‘suc 𝑖)))
104		simpr1 1213	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → 𝑓 Fn suc suc suc 𝑖)
105		sssucid 6452	. . . . . . . . . . . . . . . . . . 19 ⊢ suc suc 𝑖 ⊆ suc suc suc 𝑖
106		fnssres 6673	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 Fn suc suc suc 𝑖 ∧ suc suc 𝑖 ⊆ suc suc suc 𝑖) → (𝑓 ↾ suc suc 𝑖) Fn suc suc 𝑖)
107	104, 105, 106	sylancl 598	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓 ↾ suc suc 𝑖) Fn suc suc 𝑖)
108		peano2 7911	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ ω → suc 𝑖 ∈ ω)
109	108	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → suc 𝑖 ∈ ω)
110		nnord 7895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc 𝑖 ∈ ω → Ord suc 𝑖)
111	109, 110	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → Ord suc 𝑖)
112		0elsuc 7856	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Ord suc 𝑖 → ∅ ∈ suc suc 𝑖)
113	111, 112	syl 18	. . . . . . . . . . . . . . . . . . . 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 1251	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘∅) = 𝑥)
116	114, 115	eqtrd 2798	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥)
117		vex 3458	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑖 ∈ V
118	117	sucex 7830	. . . . . . . . . . . . . . . . . . . 20 ⊢ suc 𝑖 ∈ V
119	118	sucid 6454	. . . . . . . . . . . . . . . . . . 19 ⊢ suc 𝑖 ∈ suc suc 𝑖
120		fvres 6915	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑖 ∈ suc suc 𝑖 → ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖) = (𝑓‘suc 𝑖))
121	119, 120	mp1i 14	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖) = (𝑓‘suc 𝑖))
122		simplr3 1236	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))
123		elelsuc 6445	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 ∈ suc 𝑖 → 𝑏 ∈ suc suc 𝑖)
124	123	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → 𝑏 ∈ suc suc 𝑖)
125	35, 122, 124	rspcdva 3581	. . . . . . . . . . . . . . . . . . . 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 7843	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord suc 𝑖 → (𝑏 ∈ suc 𝑖 ↔ suc 𝑏 ∈ suc suc 𝑖))
128	111, 127	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑏 ∈ suc 𝑖 ↔ suc 𝑏 ∈ suc suc 𝑖))
129	128	biimpa 482	. . . . . . . . . . . . . . . . . . . . 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 5140	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) ∧ 𝑏 ∈ suc 𝑖) → ((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏))
132	131	ralrimiva 3158	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑏 ∈ suc 𝑖((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏))
133		vex 3458	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑓 ∈ V
134	133	resex 6024	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ↾ suc suc 𝑖) ∈ V
135		fneq1 6641	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔 Fn suc suc 𝑖 ↔ (𝑓 ↾ suc suc 𝑖) Fn suc suc 𝑖))
136		fveq1 6895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘∅) = ((𝑓 ↾ suc suc 𝑖)‘∅))
137	136	eqeq1d 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → ((𝑔‘∅) = 𝑥 ↔ ((𝑓 ↾ suc suc 𝑖)‘∅) = 𝑥))
138		fveq1 6895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (𝑔‘suc 𝑖) = ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖))
139	138	eqeq1d 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → ((𝑔‘suc 𝑖) = (𝑓‘suc 𝑖) ↔ ((𝑓 ↾ suc suc 𝑖)‘suc 𝑖) = (𝑓‘suc 𝑖)))
140	137, 139	anbi12d 644	. . . . . . . . . . . . . . . . . . . 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 5119	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → ((𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ ((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏)))
144	143	ralbidv 3189	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑓 ↾ suc suc 𝑖) → (∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏) ↔ ∀𝑏 ∈ suc 𝑖((𝑓 ↾ suc suc 𝑖)‘𝑏)𝑅((𝑓 ↾ suc suc 𝑖)‘suc 𝑏)))
145	135, 140, 144	3anbi123d 1464	. . . . . . . . . . . . . . . . . . 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 3564	. . . . . . . . . . . . . . . . . 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 1402	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)))
148		simplrl 789	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → 𝑅 ⊆ 𝑆)
149		simpr3 1215	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))
150		ssbr 5152	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ⊆ 𝑆 → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) → (𝑓‘𝑎)𝑆(𝑓‘suc 𝑎)))
151	150	ralimdv 3180	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ⊆ 𝑆 → (∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) → ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑆(𝑓‘suc 𝑎)))
152	148, 149, 151	sylc 66	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑆(𝑓‘suc 𝑎))
153		fveq2 6896	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = suc 𝑖 → (𝑓‘𝑎) = (𝑓‘suc 𝑖))
154		suceq 6438	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = suc 𝑖 → suc 𝑎 = suc suc 𝑖)
155	154	fveq2d 6900	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = suc 𝑖 → (𝑓‘suc 𝑎) = (𝑓‘suc suc 𝑖))
156	153, 155	breq12d 5119	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = suc 𝑖 → ((𝑓‘𝑎)𝑆(𝑓‘suc 𝑎) ↔ (𝑓‘suc 𝑖)𝑆(𝑓‘suc suc 𝑖)))
157	156	rspcv 3576	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑖 ∈ suc suc 𝑖 → (∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑆(𝑓‘suc 𝑎) → (𝑓‘suc 𝑖)𝑆(𝑓‘suc suc 𝑖)))
158	119, 152, 157	mpsyl 69	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc 𝑖)𝑆(𝑓‘suc suc 𝑖))
159		simpr2r 1252	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc suc 𝑖) = 𝑦)
160	158, 159	breqtrd 5134	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑓‘suc 𝑖)𝑆𝑦)
161		breq1 5109	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = (𝑓‘suc 𝑖) → (𝑧𝑆𝑦 ↔ (𝑓‘suc 𝑖)𝑆𝑦))
162	101, 161	anbi12d 644	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = (𝑓‘suc 𝑖) → ((𝑥𝑆𝑧 ∧ 𝑧𝑆𝑦) ↔ (𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦)))
163	96, 162	spcev 3564	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦) → ∃𝑧(𝑥𝑆𝑧 ∧ 𝑧𝑆𝑦))
164		vex 3458	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
165		vex 3458	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
166	164, 165	brco 5853	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥(𝑆 ∘ 𝑆)𝑦 ↔ ∃𝑧(𝑥𝑆𝑧 ∧ 𝑧𝑆𝑦))
167	163, 166	sylibr 237	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦) → 𝑥(𝑆 ∘ 𝑆)𝑦)
168		simplrr 790	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑆 ∘ 𝑆) ⊆ 𝑆)
169	168	ssbrd 5151	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑥(𝑆 ∘ 𝑆)𝑦 → 𝑥𝑆𝑦))
170	167, 169	syl5 35	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ((𝑥𝑆(𝑓‘suc 𝑖) ∧ (𝑓‘suc 𝑖)𝑆𝑦) → 𝑥𝑆𝑦))
171	160, 170	mpan2d 707	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → (𝑥𝑆(𝑓‘suc 𝑖) → 𝑥𝑆𝑦))
172	147, 171	embantd 60	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) ∧ (𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) → ((∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆(𝑓‘suc 𝑖)) → 𝑥𝑆𝑦))
173	172	ex 418	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) → ((𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → ((∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆(𝑓‘suc 𝑖)) → 𝑥𝑆𝑦)))
174	173	com23 87	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) → ((∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = (𝑓‘suc 𝑖)) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆(𝑓‘suc 𝑖)) → ((𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
175	103, 174	syl5 35	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) → (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧) → ((𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
176	175	3impia 1135	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)) → ((𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
177	176	exlimdv 1967	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)) → (∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
178	177	alrimiv 1961	. . . . . . . . . 10 ⊢ ((𝑖 ∈ ω ∧ (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
179	178	3exp 1137	. . . . . . . . 9 ⊢ (𝑖 ∈ ω → ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))))
180	179	a2d 30	. . . . . . . 8 ⊢ (𝑖 ∈ ω → (((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑖 ∧ ((𝑔‘∅) = 𝑥 ∧ (𝑔‘suc 𝑖) = 𝑧) ∧ ∀𝑏 ∈ suc 𝑖(𝑔‘𝑏)𝑅(𝑔‘suc 𝑏)) → 𝑥𝑆𝑧)) → ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑖 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc suc 𝑖) = 𝑦) ∧ ∀𝑎 ∈ suc suc 𝑖(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))))
181	24, 63, 75, 87, 95, 180	finds 7918	. . . . . . 7 ⊢ (𝑛 ∈ ω → ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
182	181	com12 33	. . . . . 6 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → (𝑛 ∈ ω → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦)))
183	182	ralrimiv 3157	. . . . 5 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑛 ∈ ω ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
184		ralcom4 3292	. . . . . 6 ⊢ (∀𝑛 ∈ ω ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦∀𝑛 ∈ ω (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
185		r19.23v 3193	. . . . . . 7 ⊢ (∀𝑛 ∈ ω (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
186	185	albii 1851	. . . . . 6 ⊢ (∀𝑦∀𝑛 ∈ ω (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
187	184, 186	bitri 278	. . . . 5 ⊢ (∀𝑛 ∈ ω ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
188	183, 187	sylib 221	. . . 4 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦))
189		brttrcl2 9728	. . . . . . 7 ⊢ (𝑥t++𝑅𝑦 ↔ ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
190		df-br 5107	. . . . . . 7 ⊢ (𝑥t++𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
191	189, 190	bitr3i 280	. . . . . 6 ⊢ (∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
192		df-br 5107	. . . . . 6 ⊢ (𝑥𝑆𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑆)
193	191, 192	imbi12i 353	. . . . 5 ⊢ ((∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ (⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
194	193	albii 1851	. . . 4 ⊢ (∀𝑦(∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘suc 𝑛) = 𝑦) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) → 𝑥𝑆𝑦) ↔ ∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
195	188, 194	sylib 221	. . 3 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
196	195	alrimiv 1961	. 2 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
197		relttrcl 9726	. . 3 ⊢ Rel t++𝑅
198		ssrel 5764	. . 3 ⊢ (Rel t++𝑅 → (t++𝑅 ⊆ 𝑆 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆)))
199	197, 198	ax-mp 5	. 2 ⊢ (t++𝑅 ⊆ 𝑆 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ t++𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆))
200	196, 199	sylibr 237	1 ⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → t++𝑅 ⊆ 𝑆)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 ∀wal 1567 = wceq 1569 ∃wex 1811 ∈ wcel 2146 ∀wral 3080 ∃wrex 3090 ⊆ wss 3900 ∅c0 4281 {csn 4588 ⟨cop 4838 class class class wbr 5106 ↾ cres 5657 ∘ ccom 5659 Rel wrel 5660 Ord word 6368 suc csuc 6371 Fn wfn 6542 ‘cfv 6547 ωcom 7887 1_oc1o 8483 t++cttrcl 9721

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1944 ax-6 2001 ax-7 2042 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2196 ax-12 2215 ax-ext 2735 ax-sep 5252 ax-nul 5263 ax-pr 5395 ax-un 7761

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2101 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6311 df-ord 6372 df-on 6373 df-lim 6374 df-suc 6375 df-iota 6501 df-fun 6549 df-fn 6550 df-f 6551 df-f1 6552 df-fo 6553 df-f1o 6554 df-fv 6555 df-ov 7433 df-oprab 7434 df-mpo 7435 df-om 7888 df-2nd 8012 df-frecs 8313 df-wrecs 8344 df-recs 8393 df-rdg 8432 df-1o 8490 df-oadd 8494 df-ttrcl 9722

This theorem is used by: dfttrcl2 9738

W3C validator