Users' Mathboxes Mathbox for ML < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rdgssun Structured version   Visualization version   GIF version

Theorem rdgssun 36793
Description: In a recursive definition where each step expands on the previous one using a union, every previous step is a subset of every later step. (Contributed by ML, 1-Apr-2022.)
Hypotheses
Ref Expression
rdgssun.1 𝐹 = (𝑤 ∈ V ↦ (𝑤𝐵))
rdgssun.2 𝐵 ∈ V
Assertion
Ref Expression
rdgssun ((𝑋 ∈ On ∧ 𝑌𝑋) → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋))
Distinct variable groups:   𝑤,𝐴   𝑤,𝑌
Allowed substitution hints:   𝐵(𝑤)   𝐹(𝑤)   𝑋(𝑤)

Proof of Theorem rdgssun
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfsbc1v 3794 . . . . . . . . . . . 12 𝑥[∅ / 𝑥]𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)
2 0ex 5301 . . . . . . . . . . . 12 ∅ ∈ V
3 rzal 4504 . . . . . . . . . . . . 13 (𝑥 = ∅ → ∀𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥))
4 sbceq1a 3785 . . . . . . . . . . . . 13 (𝑥 = ∅ → (∀𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) ↔ [∅ / 𝑥]𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)))
53, 4mpbid 231 . . . . . . . . . . . 12 (𝑥 = ∅ → [∅ / 𝑥]𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥))
61, 2, 5vtoclef 3546 . . . . . . . . . . 11 [∅ / 𝑥]𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)
7 vex 3473 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
87elsuc 6433 . . . . . . . . . . . . . . 15 (𝑦 ∈ suc 𝑥 ↔ (𝑦𝑥𝑦 = 𝑥))
9 ssun1 4168 . . . . . . . . . . . . . . . . . . . 20 (rec(𝐹, 𝐴)‘𝑥) ⊆ ((rec(𝐹, 𝐴)‘𝑥) ∪ (rec(𝐹, 𝐴)‘𝑥) / 𝑤𝐵)
10 fvex 6904 . . . . . . . . . . . . . . . . . . . . . 22 (rec(𝐹, 𝐴)‘𝑥) ∈ V
11 rdgssun.2 . . . . . . . . . . . . . . . . . . . . . . 23 𝐵 ∈ V
1211csbex 5305 . . . . . . . . . . . . . . . . . . . . . 22 (rec(𝐹, 𝐴)‘𝑥) / 𝑤𝐵 ∈ V
1310, 12unex 7742 . . . . . . . . . . . . . . . . . . . . 21 ((rec(𝐹, 𝐴)‘𝑥) ∪ (rec(𝐹, 𝐴)‘𝑥) / 𝑤𝐵) ∈ V
14 nfcv 2898 . . . . . . . . . . . . . . . . . . . . . 22 𝑤𝐴
15 nfcv 2898 . . . . . . . . . . . . . . . . . . . . . 22 𝑤𝑥
16 rdgssun.1 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝐹 = (𝑤 ∈ V ↦ (𝑤𝐵))
17 nfmpt1 5250 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑤(𝑤 ∈ V ↦ (𝑤𝐵))
1816, 17nfcxfr 2896 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑤𝐹
1918, 14nfrdg 8428 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑤rec(𝐹, 𝐴)
2019, 15nffv 6901 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤(rec(𝐹, 𝐴)‘𝑥)
2120nfcsb1 3913 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤(rec(𝐹, 𝐴)‘𝑥) / 𝑤𝐵
2220, 21nfun 4161 . . . . . . . . . . . . . . . . . . . . . 22 𝑤((rec(𝐹, 𝐴)‘𝑥) ∪ (rec(𝐹, 𝐴)‘𝑥) / 𝑤𝐵)
23 rdgeq1 8425 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 = (𝑤 ∈ V ↦ (𝑤𝐵)) → rec(𝐹, 𝐴) = rec((𝑤 ∈ V ↦ (𝑤𝐵)), 𝐴))
2416, 23ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 rec(𝐹, 𝐴) = rec((𝑤 ∈ V ↦ (𝑤𝐵)), 𝐴)
25 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = (rec(𝐹, 𝐴)‘𝑥) → 𝑤 = (rec(𝐹, 𝐴)‘𝑥))
26 csbeq1a 3903 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = (rec(𝐹, 𝐴)‘𝑥) → 𝐵 = (rec(𝐹, 𝐴)‘𝑥) / 𝑤𝐵)
2725, 26uneq12d 4160 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = (rec(𝐹, 𝐴)‘𝑥) → (𝑤𝐵) = ((rec(𝐹, 𝐴)‘𝑥) ∪ (rec(𝐹, 𝐴)‘𝑥) / 𝑤𝐵))
2814, 15, 22, 24, 27rdgsucmptf 8442 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ On ∧ ((rec(𝐹, 𝐴)‘𝑥) ∪ (rec(𝐹, 𝐴)‘𝑥) / 𝑤𝐵) ∈ V) → (rec(𝐹, 𝐴)‘suc 𝑥) = ((rec(𝐹, 𝐴)‘𝑥) ∪ (rec(𝐹, 𝐴)‘𝑥) / 𝑤𝐵))
2913, 28mpan2 690 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ On → (rec(𝐹, 𝐴)‘suc 𝑥) = ((rec(𝐹, 𝐴)‘𝑥) ∪ (rec(𝐹, 𝐴)‘𝑥) / 𝑤𝐵))
309, 29sseqtrrid 4031 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ On → (rec(𝐹, 𝐴)‘𝑥) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥))
31 sstr2 3985 . . . . . . . . . . . . . . . . . . 19 ((rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) → ((rec(𝐹, 𝐴)‘𝑥) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥) → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥)))
3230, 31syl5com 31 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ On → ((rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥)))
3332imim2d 57 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ On → ((𝑦𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)) → (𝑦𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥))))
3433imp 406 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ On ∧ (𝑦𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥))) → (𝑦𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥)))
35 fveq2 6891 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑥 → (rec(𝐹, 𝐴)‘𝑦) = (rec(𝐹, 𝐴)‘𝑥))
3635sseq1d 4009 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑥 → ((rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥) ↔ (rec(𝐹, 𝐴)‘𝑥) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥)))
3730, 36syl5ibrcom 246 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ On → (𝑦 = 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥)))
3837adantr 480 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ On ∧ (𝑦𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥))) → (𝑦 = 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥)))
3934, 38jaod 858 . . . . . . . . . . . . . . 15 ((𝑥 ∈ On ∧ (𝑦𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥))) → ((𝑦𝑥𝑦 = 𝑥) → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥)))
408, 39biimtrid 241 . . . . . . . . . . . . . 14 ((𝑥 ∈ On ∧ (𝑦𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥))) → (𝑦 ∈ suc 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥)))
4140ex 412 . . . . . . . . . . . . 13 (𝑥 ∈ On → ((𝑦𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)) → (𝑦 ∈ suc 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥))))
4241ralimdv2 3158 . . . . . . . . . . . 12 (𝑥 ∈ On → (∀𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) → ∀𝑦 ∈ suc 𝑥(rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥)))
43 df-sbc 3775 . . . . . . . . . . . . 13 ([suc 𝑥 / 𝑥]𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) ↔ suc 𝑥 ∈ {𝑥 ∣ ∀𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)})
44 vex 3473 . . . . . . . . . . . . . . 15 𝑥 ∈ V
4544sucex 7803 . . . . . . . . . . . . . 14 suc 𝑥 ∈ V
46 fveq2 6891 . . . . . . . . . . . . . . . 16 (𝑧 = suc 𝑥 → (rec(𝐹, 𝐴)‘𝑧) = (rec(𝐹, 𝐴)‘suc 𝑥))
4746sseq2d 4010 . . . . . . . . . . . . . . 15 (𝑧 = suc 𝑥 → ((rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧) ↔ (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥)))
4847raleqbi1dv 3328 . . . . . . . . . . . . . 14 (𝑧 = suc 𝑥 → (∀𝑦𝑧 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧) ↔ ∀𝑦 ∈ suc 𝑥(rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥)))
49 fveq2 6891 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → (rec(𝐹, 𝐴)‘𝑥) = (rec(𝐹, 𝐴)‘𝑧))
5049sseq2d 4010 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → ((rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) ↔ (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧)))
5150raleqbi1dv 3328 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → (∀𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) ↔ ∀𝑦𝑧 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧)))
5251cbvabv 2800 . . . . . . . . . . . . . 14 {𝑥 ∣ ∀𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)} = {𝑧 ∣ ∀𝑦𝑧 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧)}
5345, 48, 52elab2 3669 . . . . . . . . . . . . 13 (suc 𝑥 ∈ {𝑥 ∣ ∀𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)} ↔ ∀𝑦 ∈ suc 𝑥(rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥))
5443, 53bitri 275 . . . . . . . . . . . 12 ([suc 𝑥 / 𝑥]𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) ↔ ∀𝑦 ∈ suc 𝑥(rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥))
5542, 54imbitrrdi 251 . . . . . . . . . . 11 (𝑥 ∈ On → (∀𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) → [suc 𝑥 / 𝑥]𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)))
56 ssiun2 5044 . . . . . . . . . . . . . . . 16 (𝑦𝑧 → (rec(𝐹, 𝐴)‘𝑦) ⊆ 𝑦𝑧 (rec(𝐹, 𝐴)‘𝑦))
5756adantl 481 . . . . . . . . . . . . . . 15 ((Lim 𝑧𝑦𝑧) → (rec(𝐹, 𝐴)‘𝑦) ⊆ 𝑦𝑧 (rec(𝐹, 𝐴)‘𝑦))
58 vex 3473 . . . . . . . . . . . . . . . . 17 𝑧 ∈ V
59 rdglim2a 8447 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ V ∧ Lim 𝑧) → (rec(𝐹, 𝐴)‘𝑧) = 𝑦𝑧 (rec(𝐹, 𝐴)‘𝑦))
6058, 59mpan 689 . . . . . . . . . . . . . . . 16 (Lim 𝑧 → (rec(𝐹, 𝐴)‘𝑧) = 𝑦𝑧 (rec(𝐹, 𝐴)‘𝑦))
6160adantr 480 . . . . . . . . . . . . . . 15 ((Lim 𝑧𝑦𝑧) → (rec(𝐹, 𝐴)‘𝑧) = 𝑦𝑧 (rec(𝐹, 𝐴)‘𝑦))
6257, 61sseqtrrd 4019 . . . . . . . . . . . . . 14 ((Lim 𝑧𝑦𝑧) → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧))
6362ralrimiva 3141 . . . . . . . . . . . . 13 (Lim 𝑧 → ∀𝑦𝑧 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧))
64 df-sbc 3775 . . . . . . . . . . . . . . 15 ([𝑧 / 𝑥]𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) ↔ 𝑧 ∈ {𝑥 ∣ ∀𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)})
6552eleq2i 2820 . . . . . . . . . . . . . . 15 (𝑧 ∈ {𝑥 ∣ ∀𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)} ↔ 𝑧 ∈ {𝑧 ∣ ∀𝑦𝑧 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧)})
6664, 65bitri 275 . . . . . . . . . . . . . 14 ([𝑧 / 𝑥]𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) ↔ 𝑧 ∈ {𝑧 ∣ ∀𝑦𝑧 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧)})
67 abid 2708 . . . . . . . . . . . . . 14 (𝑧 ∈ {𝑧 ∣ ∀𝑦𝑧 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧)} ↔ ∀𝑦𝑧 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧))
6866, 67bitri 275 . . . . . . . . . . . . 13 ([𝑧 / 𝑥]𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) ↔ ∀𝑦𝑧 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧))
6963, 68sylibr 233 . . . . . . . . . . . 12 (Lim 𝑧[𝑧 / 𝑥]𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥))
7069a1d 25 . . . . . . . . . . 11 (Lim 𝑧 → (∀𝑥𝑧𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) → [𝑧 / 𝑥]𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)))
716, 55, 70tfindes 7861 . . . . . . . . . 10 (𝑥 ∈ On → ∀𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥))
72 rsp 3239 . . . . . . . . . 10 (∀𝑦𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) → (𝑦𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)))
7371, 72syl 17 . . . . . . . . 9 (𝑥 ∈ On → (𝑦𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)))
74 eleq1 2816 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝑥 ∈ On ↔ 𝑋 ∈ On))
7574adantl 481 . . . . . . . . . 10 ((𝑦 = 𝑌𝑥 = 𝑋) → (𝑥 ∈ On ↔ 𝑋 ∈ On))
76 eleq12 2818 . . . . . . . . . . 11 ((𝑦 = 𝑌𝑥 = 𝑋) → (𝑦𝑥𝑌𝑋))
77 fveq2 6891 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → (rec(𝐹, 𝐴)‘𝑦) = (rec(𝐹, 𝐴)‘𝑌))
7877adantr 480 . . . . . . . . . . . 12 ((𝑦 = 𝑌𝑥 = 𝑋) → (rec(𝐹, 𝐴)‘𝑦) = (rec(𝐹, 𝐴)‘𝑌))
79 fveq2 6891 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → (rec(𝐹, 𝐴)‘𝑥) = (rec(𝐹, 𝐴)‘𝑋))
8079adantl 481 . . . . . . . . . . . 12 ((𝑦 = 𝑌𝑥 = 𝑋) → (rec(𝐹, 𝐴)‘𝑥) = (rec(𝐹, 𝐴)‘𝑋))
8178, 80sseq12d 4011 . . . . . . . . . . 11 ((𝑦 = 𝑌𝑥 = 𝑋) → ((rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) ↔ (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋)))
8276, 81imbi12d 344 . . . . . . . . . 10 ((𝑦 = 𝑌𝑥 = 𝑋) → ((𝑦𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)) ↔ (𝑌𝑋 → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋))))
8375, 82imbi12d 344 . . . . . . . . 9 ((𝑦 = 𝑌𝑥 = 𝑋) → ((𝑥 ∈ On → (𝑦𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥))) ↔ (𝑋 ∈ On → (𝑌𝑋 → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋)))))
8473, 83mpbii 232 . . . . . . . 8 ((𝑦 = 𝑌𝑥 = 𝑋) → (𝑋 ∈ On → (𝑌𝑋 → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋))))
8584ex 412 . . . . . . 7 (𝑦 = 𝑌 → (𝑥 = 𝑋 → (𝑋 ∈ On → (𝑌𝑋 → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋)))))
8685vtocleg 3537 . . . . . 6 (𝑌𝑋 → (𝑥 = 𝑋 → (𝑋 ∈ On → (𝑌𝑋 → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋)))))
8786com12 32 . . . . 5 (𝑥 = 𝑋 → (𝑌𝑋 → (𝑋 ∈ On → (𝑌𝑋 → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋)))))
8887vtocleg 3537 . . . 4 (𝑋 ∈ On → (𝑌𝑋 → (𝑋 ∈ On → (𝑌𝑋 → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋)))))
8988pm2.43b 55 . . 3 (𝑌𝑋 → (𝑋 ∈ On → (𝑌𝑋 → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋))))
9089pm2.43b 55 . 2 (𝑋 ∈ On → (𝑌𝑋 → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋)))
9190imp 406 1 ((𝑋 ∈ On ∧ 𝑌𝑋) → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  wo 846   = wceq 1534  wcel 2099  {cab 2704  wral 3056  Vcvv 3469  [wsbc 3774  csb 3889  cun 3942  wss 3944  c0 4318   ciun 4991  cmpt 5225  Oncon0 6363  Lim wlim 6364  suc csuc 6365  cfv 6542  reccrdg 8423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7734
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator