Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  rdgss GIF version

Theorem rdgss 6292
 Description: Subset and recursive definition generator. (Contributed by Jim Kingdon, 15-Jul-2019.)
Hypotheses
Ref Expression
rdgss.1 (𝜑𝐹 Fn V)
rdgss.2 (𝜑𝐼𝑉)
rdgss.3 (𝜑𝐴 ∈ On)
rdgss.4 (𝜑𝐵 ∈ On)
rdgss.5 (𝜑𝐴𝐵)
Assertion
Ref Expression
rdgss (𝜑 → (rec(𝐹, 𝐼)‘𝐴) ⊆ (rec(𝐹, 𝐼)‘𝐵))

Proof of Theorem rdgss
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rdgss.5 . . . 4 (𝜑𝐴𝐵)
2 ssel 3098 . . . . . 6 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
3 ssid 3124 . . . . . . 7 (𝐹‘(rec(𝐹, 𝐼)‘𝑥)) ⊆ (𝐹‘(rec(𝐹, 𝐼)‘𝑥))
4 fveq2 5433 . . . . . . . . . 10 (𝑦 = 𝑥 → (rec(𝐹, 𝐼)‘𝑦) = (rec(𝐹, 𝐼)‘𝑥))
54fveq2d 5437 . . . . . . . . 9 (𝑦 = 𝑥 → (𝐹‘(rec(𝐹, 𝐼)‘𝑦)) = (𝐹‘(rec(𝐹, 𝐼)‘𝑥)))
65sseq2d 3134 . . . . . . . 8 (𝑦 = 𝑥 → ((𝐹‘(rec(𝐹, 𝐼)‘𝑥)) ⊆ (𝐹‘(rec(𝐹, 𝐼)‘𝑦)) ↔ (𝐹‘(rec(𝐹, 𝐼)‘𝑥)) ⊆ (𝐹‘(rec(𝐹, 𝐼)‘𝑥))))
76rspcev 2795 . . . . . . 7 ((𝑥𝐵 ∧ (𝐹‘(rec(𝐹, 𝐼)‘𝑥)) ⊆ (𝐹‘(rec(𝐹, 𝐼)‘𝑥))) → ∃𝑦𝐵 (𝐹‘(rec(𝐹, 𝐼)‘𝑥)) ⊆ (𝐹‘(rec(𝐹, 𝐼)‘𝑦)))
83, 7mpan2 422 . . . . . 6 (𝑥𝐵 → ∃𝑦𝐵 (𝐹‘(rec(𝐹, 𝐼)‘𝑥)) ⊆ (𝐹‘(rec(𝐹, 𝐼)‘𝑦)))
92, 8syl6 33 . . . . 5 (𝐴𝐵 → (𝑥𝐴 → ∃𝑦𝐵 (𝐹‘(rec(𝐹, 𝐼)‘𝑥)) ⊆ (𝐹‘(rec(𝐹, 𝐼)‘𝑦))))
109ralrimiv 2509 . . . 4 (𝐴𝐵 → ∀𝑥𝐴𝑦𝐵 (𝐹‘(rec(𝐹, 𝐼)‘𝑥)) ⊆ (𝐹‘(rec(𝐹, 𝐼)‘𝑦)))
111, 10syl 14 . . 3 (𝜑 → ∀𝑥𝐴𝑦𝐵 (𝐹‘(rec(𝐹, 𝐼)‘𝑥)) ⊆ (𝐹‘(rec(𝐹, 𝐼)‘𝑦)))
12 iunss2 3868 . . 3 (∀𝑥𝐴𝑦𝐵 (𝐹‘(rec(𝐹, 𝐼)‘𝑥)) ⊆ (𝐹‘(rec(𝐹, 𝐼)‘𝑦)) → 𝑥𝐴 (𝐹‘(rec(𝐹, 𝐼)‘𝑥)) ⊆ 𝑦𝐵 (𝐹‘(rec(𝐹, 𝐼)‘𝑦)))
13 unss2 3254 . . 3 ( 𝑥𝐴 (𝐹‘(rec(𝐹, 𝐼)‘𝑥)) ⊆ 𝑦𝐵 (𝐹‘(rec(𝐹, 𝐼)‘𝑦)) → (𝐼 𝑥𝐴 (𝐹‘(rec(𝐹, 𝐼)‘𝑥))) ⊆ (𝐼 𝑦𝐵 (𝐹‘(rec(𝐹, 𝐼)‘𝑦))))
1411, 12, 133syl 17 . 2 (𝜑 → (𝐼 𝑥𝐴 (𝐹‘(rec(𝐹, 𝐼)‘𝑥))) ⊆ (𝐼 𝑦𝐵 (𝐹‘(rec(𝐹, 𝐼)‘𝑦))))
15 rdgss.1 . . 3 (𝜑𝐹 Fn V)
16 rdgss.2 . . 3 (𝜑𝐼𝑉)
17 rdgss.3 . . 3 (𝜑𝐴 ∈ On)
18 rdgival 6291 . . 3 ((𝐹 Fn V ∧ 𝐼𝑉𝐴 ∈ On) → (rec(𝐹, 𝐼)‘𝐴) = (𝐼 𝑥𝐴 (𝐹‘(rec(𝐹, 𝐼)‘𝑥))))
1915, 16, 17, 18syl3anc 1217 . 2 (𝜑 → (rec(𝐹, 𝐼)‘𝐴) = (𝐼 𝑥𝐴 (𝐹‘(rec(𝐹, 𝐼)‘𝑥))))
20 rdgss.4 . . 3 (𝜑𝐵 ∈ On)
21 rdgival 6291 . . 3 ((𝐹 Fn V ∧ 𝐼𝑉𝐵 ∈ On) → (rec(𝐹, 𝐼)‘𝐵) = (𝐼 𝑦𝐵 (𝐹‘(rec(𝐹, 𝐼)‘𝑦))))
2215, 16, 20, 21syl3anc 1217 . 2 (𝜑 → (rec(𝐹, 𝐼)‘𝐵) = (𝐼 𝑦𝐵 (𝐹‘(rec(𝐹, 𝐼)‘𝑦))))
2314, 19, 223sstr4d 3149 1 (𝜑 → (rec(𝐹, 𝐼)‘𝐴) ⊆ (rec(𝐹, 𝐼)‘𝐵))
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1332   ∈ wcel 2112  ∀wral 2418  ∃wrex 2419  Vcvv 2691   ∪ cun 3076   ⊆ wss 3078  ∪ ciun 3823  Oncon0 4296   Fn wfn 5130  ‘cfv 5135  reccrdg 6278 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-13 2114  ax-14 2115  ax-ext 2123  ax-coll 4053  ax-sep 4056  ax-pow 4108  ax-pr 4142  ax-un 4366  ax-setind 4463 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1732  df-eu 1993  df-mo 1994  df-clab 2128  df-cleq 2134  df-clel 2137  df-nfc 2272  df-ne 2311  df-ral 2423  df-rex 2424  df-reu 2425  df-rab 2427  df-v 2693  df-sbc 2916  df-csb 3010  df-dif 3080  df-un 3082  df-in 3084  df-ss 3091  df-nul 3371  df-pw 3519  df-sn 3540  df-pr 3541  df-op 3543  df-uni 3747  df-iun 3825  df-br 3940  df-opab 4000  df-mpt 4001  df-tr 4037  df-id 4226  df-iord 4299  df-on 4301  df-suc 4304  df-xp 4557  df-rel 4558  df-cnv 4559  df-co 4560  df-dm 4561  df-rn 4562  df-res 4563  df-ima 4564  df-iota 5100  df-fun 5137  df-fn 5138  df-f 5139  df-f1 5140  df-fo 5141  df-f1o 5142  df-fv 5143  df-recs 6214  df-irdg 6279 This theorem is referenced by:  oawordi  6377
 Copyright terms: Public domain W3C validator