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

Theorem trpredmintr 33184
Description: The transitive predecessors form the smallest class transitive in 𝑅 and 𝐴. That is, if 𝐵 is another 𝑅, 𝐴 transitive class containing Pred(𝑅, 𝐴, 𝑋), then TrPred(𝑅, 𝐴, 𝑋) ⊆ 𝐵 (Contributed by Scott Fenton, 25-Apr-2012.) (Revised by Mario Carneiro, 26-Jun-2015.)
Assertion
Ref Expression
trpredmintr (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → TrPred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)
Distinct variable groups:   𝑦,𝐴   𝑦,𝐵   𝑦,𝑅   𝑦,𝑋

Proof of Theorem trpredmintr
Dummy variables 𝑎 𝑐 𝑑 𝑖 𝑗 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dftrpred2 33172 . 2 TrPred(𝑅, 𝐴, 𝑋) = 𝑖 ∈ ω ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)
2 fveq2 6649 . . . . . . . 8 (𝑗 = ∅ → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) = ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅))
32sseq1d 3949 . . . . . . 7 (𝑗 = ∅ → (((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵 ↔ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) ⊆ 𝐵))
43imbi2d 344 . . . . . 6 (𝑗 = ∅ → ((((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵) ↔ (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) ⊆ 𝐵)))
5 fveq2 6649 . . . . . . . 8 (𝑗 = 𝑘 → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) = ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘))
65sseq1d 3949 . . . . . . 7 (𝑗 = 𝑘 → (((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵 ↔ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵))
76imbi2d 344 . . . . . 6 (𝑗 = 𝑘 → ((((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵) ↔ (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)))
8 fveq2 6649 . . . . . . . 8 (𝑗 = suc 𝑘 → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) = ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘))
98sseq1d 3949 . . . . . . 7 (𝑗 = suc 𝑘 → (((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵 ↔ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘) ⊆ 𝐵))
109imbi2d 344 . . . . . 6 (𝑗 = suc 𝑘 → ((((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵) ↔ (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘) ⊆ 𝐵)))
11 fveq2 6649 . . . . . . . 8 (𝑗 = 𝑖 → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) = ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖))
1211sseq1d 3949 . . . . . . 7 (𝑗 = 𝑖 → (((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵 ↔ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵))
1312imbi2d 344 . . . . . 6 (𝑗 = 𝑖 → ((((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐵) ↔ (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵)))
14 setlikespec 6141 . . . . . . . . 9 ((𝑋𝐴𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑋) ∈ V)
15 fr0g 8058 . . . . . . . . 9 (Pred(𝑅, 𝐴, 𝑋) ∈ V → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) = Pred(𝑅, 𝐴, 𝑋))
1614, 15syl 17 . . . . . . . 8 ((𝑋𝐴𝑅 Se 𝐴) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) = Pred(𝑅, 𝐴, 𝑋))
1716adantr 484 . . . . . . 7 (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) = Pred(𝑅, 𝐴, 𝑋))
18 simprr 772 . . . . . . 7 (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)
1917, 18eqsstrd 3956 . . . . . 6 (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) ⊆ 𝐵)
20 fvex 6662 . . . . . . . . . . 11 ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ∈ V
21 trpredlem1 33180 . . . . . . . . . . . . . . . 16 (Pred(𝑅, 𝐴, 𝑋) ∈ V → ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐴)
2214, 21syl 17 . . . . . . . . . . . . . . 15 ((𝑋𝐴𝑅 Se 𝐴) → ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐴)
2322sseld 3917 . . . . . . . . . . . . . 14 ((𝑋𝐴𝑅 Se 𝐴) → (𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) → 𝑦𝐴))
24 setlikespec 6141 . . . . . . . . . . . . . . . 16 ((𝑦𝐴𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑦) ∈ V)
2524expcom 417 . . . . . . . . . . . . . . 15 (𝑅 Se 𝐴 → (𝑦𝐴 → Pred(𝑅, 𝐴, 𝑦) ∈ V))
2625adantl 485 . . . . . . . . . . . . . 14 ((𝑋𝐴𝑅 Se 𝐴) → (𝑦𝐴 → Pred(𝑅, 𝐴, 𝑦) ∈ V))
2723, 26syld 47 . . . . . . . . . . . . 13 ((𝑋𝐴𝑅 Se 𝐴) → (𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) → Pred(𝑅, 𝐴, 𝑦) ∈ V))
2827ralrimiv 3151 . . . . . . . . . . . 12 ((𝑋𝐴𝑅 Se 𝐴) → ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ∈ V)
2928ad2antrr 725 . . . . . . . . . . 11 ((((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵) → ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ∈ V)
30 iunexg 7650 . . . . . . . . . . 11 ((((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ∈ V ∧ ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ∈ V) → 𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ∈ V)
3120, 29, 30sylancr 590 . . . . . . . . . 10 ((((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵) → 𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ∈ V)
32 nfcv 2958 . . . . . . . . . . 11 𝑎Pred(𝑅, 𝐴, 𝑋)
33 nfcv 2958 . . . . . . . . . . 11 𝑎𝑘
34 nfcv 2958 . . . . . . . . . . 11 𝑎 𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦)
35 eqid 2801 . . . . . . . . . . 11 (rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω) = (rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)
36 predeq3 6124 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑑 → Pred(𝑅, 𝐴, 𝑦) = Pred(𝑅, 𝐴, 𝑑))
3736cbviunv 4930 . . . . . . . . . . . . . . . . 17 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦) = 𝑑𝑎 Pred(𝑅, 𝐴, 𝑑)
38 iuneq1 4900 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑐 𝑑𝑎 Pred(𝑅, 𝐴, 𝑑) = 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑))
3937, 38syl5eq 2848 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑐 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦) = 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑))
4039cbvmptv 5136 . . . . . . . . . . . . . . 15 (𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)) = (𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑))
41 rdgeq1 8034 . . . . . . . . . . . . . . 15 ((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)) = (𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)) → rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) = rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)))
42 reseq1 5816 . . . . . . . . . . . . . . 15 (rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) = rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) → (rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω) = (rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω))
4340, 41, 42mp2b 10 . . . . . . . . . . . . . 14 (rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω) = (rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)
4443fveq1i 6650 . . . . . . . . . . . . 13 ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) = ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)
4544eqeq2i 2814 . . . . . . . . . . . 12 (𝑎 = ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ↔ 𝑎 = ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘))
46 iuneq1 4900 . . . . . . . . . . . 12 (𝑎 = ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) → 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦) = 𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦))
4745, 46sylbi 220 . . . . . . . . . . 11 (𝑎 = ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) → 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦) = 𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦))
4832, 33, 34, 35, 47frsucmpt 8060 . . . . . . . . . 10 ((𝑘 ∈ ω ∧ 𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ∈ V) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘) = 𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦))
4931, 48sylan2 595 . . . . . . . . 9 ((𝑘 ∈ ω ∧ (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘) = 𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦))
5044sseq1i 3946 . . . . . . . . . . . 12 (((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵 ↔ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)
5150anbi2i 625 . . . . . . . . . . 11 ((((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵) ↔ (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵))
52 nfv 1915 . . . . . . . . . . . . . . 15 𝑦(𝑋𝐴𝑅 Se 𝐴)
53 nfra1 3186 . . . . . . . . . . . . . . . 16 𝑦𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵
54 nfv 1915 . . . . . . . . . . . . . . . 16 𝑦Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵
5553, 54nfan 1900 . . . . . . . . . . . . . . 15 𝑦(∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)
5652, 55nfan 1900 . . . . . . . . . . . . . 14 𝑦((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵))
57 nfv 1915 . . . . . . . . . . . . . 14 𝑦((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵
5856, 57nfan 1900 . . . . . . . . . . . . 13 𝑦(((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)
59 ssel 3911 . . . . . . . . . . . . . 14 (((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵 → (𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) → 𝑦𝐵))
60 rsp 3173 . . . . . . . . . . . . . . 15 (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → (𝑦𝐵 → Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵))
6160ad2antrl 727 . . . . . . . . . . . . . 14 (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → (𝑦𝐵 → Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵))
6259, 61sylan9r 512 . . . . . . . . . . . . 13 ((((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵) → (𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) → Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵))
6358, 62ralrimi 3183 . . . . . . . . . . . 12 ((((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵) → ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵)
6463adantl 485 . . . . . . . . . . 11 ((𝑘 ∈ ω ∧ (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)) → ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵)
6551, 64sylan2b 596 . . . . . . . . . 10 ((𝑘 ∈ ω ∧ (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)) → ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵)
66 iunss 4935 . . . . . . . . . 10 ( 𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ↔ ∀𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵)
6765, 66sylibr 237 . . . . . . . . 9 ((𝑘 ∈ ω ∧ (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)) → 𝑦 ∈ ((rec((𝑐 ∈ V ↦ 𝑑𝑐 Pred(𝑅, 𝐴, 𝑑)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘)Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵)
6849, 67eqsstrd 3956 . . . . . . . 8 ((𝑘 ∈ ω ∧ (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) ∧ ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘) ⊆ 𝐵)
6968exp32 424 . . . . . . 7 (𝑘 ∈ ω → (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → (((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵 → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘) ⊆ 𝐵)))
7069a2d 29 . . . . . 6 (𝑘 ∈ ω → ((((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑘) ⊆ 𝐵) → (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑘) ⊆ 𝐵)))
714, 7, 10, 13, 19, 70finds 7593 . . . . 5 (𝑖 ∈ ω → (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵))
7271com12 32 . . . 4 (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → (𝑖 ∈ ω → ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵))
7372ralrimiv 3151 . . 3 (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → ∀𝑖 ∈ ω ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵)
74 iunss 4935 . . 3 ( 𝑖 ∈ ω ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵 ↔ ∀𝑖 ∈ ω ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵)
7573, 74sylibr 237 . 2 (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → 𝑖 ∈ ω ((rec((𝑎 ∈ V ↦ 𝑦𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐵)
761, 75eqsstrid 3966 1 (((𝑋𝐴𝑅 Se 𝐴) ∧ (∀𝑦𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → TrPred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2112  wral 3109  Vcvv 3444  wss 3884  c0 4246   ciun 4884  cmpt 5113   Se wse 5480  cres 5525  Predcpred 6119  suc csuc 6165  cfv 6328  ωcom 7564  reccrdg 8032  TrPredctrpred 33170
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-trpred 33171
This theorem is referenced by:  trpredelss  33185  dftrpred3g  33186  trpredpo  33188
  Copyright terms: Public domain W3C validator