![]() |
Mathbox for Jonathan Ben-Naim |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > bnj1030 | Structured version Visualization version GIF version |
Description: Technical lemma for bnj69 34774. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
Ref | Expression |
---|---|
bnj1030.1 | ⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) |
bnj1030.2 | ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
bnj1030.3 | ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
bnj1030.4 | ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴)) |
bnj1030.5 | ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)) |
bnj1030.6 | ⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) |
bnj1030.7 | ⊢ 𝐷 = (ω ∖ {∅}) |
bnj1030.8 | ⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} |
bnj1030.9 | ⊢ (𝜂 ↔ ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)) |
bnj1030.10 | ⊢ (𝜌 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜂)) |
bnj1030.11 | ⊢ (𝜑′ ↔ [𝑗 / 𝑖]𝜑) |
bnj1030.12 | ⊢ (𝜓′ ↔ [𝑗 / 𝑖]𝜓) |
bnj1030.13 | ⊢ (𝜒′ ↔ [𝑗 / 𝑖]𝜒) |
bnj1030.14 | ⊢ (𝜃′ ↔ [𝑗 / 𝑖]𝜃) |
bnj1030.15 | ⊢ (𝜏′ ↔ [𝑗 / 𝑖]𝜏) |
bnj1030.16 | ⊢ (𝜁′ ↔ [𝑗 / 𝑖]𝜁) |
bnj1030.17 | ⊢ (𝜂′ ↔ [𝑗 / 𝑖]𝜂) |
bnj1030.18 | ⊢ (𝜎 ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′)) |
bnj1030.19 | ⊢ (𝜑0 ↔ (𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓)) |
Ref | Expression |
---|---|
bnj1030 | ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bnj1030.1 | . 2 ⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) | |
2 | bnj1030.2 | . 2 ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) | |
3 | bnj1030.3 | . 2 ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) | |
4 | bnj1030.4 | . 2 ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴)) | |
5 | bnj1030.5 | . 2 ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)) | |
6 | bnj1030.6 | . 2 ⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) | |
7 | bnj1030.7 | . 2 ⊢ 𝐷 = (ω ∖ {∅}) | |
8 | bnj1030.8 | . 2 ⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} | |
9 | 19.23vv 1938 | . . . . 5 ⊢ (∀𝑛∀𝑖((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵) ↔ (∃𝑛∃𝑖(𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵)) | |
10 | 9 | albii 1813 | . . . 4 ⊢ (∀𝑓∀𝑛∀𝑖((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵) ↔ ∀𝑓(∃𝑛∃𝑖(𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵)) |
11 | 19.23v 1937 | . . . 4 ⊢ (∀𝑓(∃𝑛∃𝑖(𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵) ↔ (∃𝑓∃𝑛∃𝑖(𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵)) | |
12 | 10, 11 | bitri 274 | . . 3 ⊢ (∀𝑓∀𝑛∀𝑖((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵) ↔ (∃𝑓∃𝑛∃𝑖(𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵)) |
13 | bnj1030.9 | . . . . 5 ⊢ (𝜂 ↔ ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)) | |
14 | 7 | bnj1071 34741 | . . . . . . . 8 ⊢ (𝑛 ∈ 𝐷 → E Fr 𝑛) |
15 | 3, 14 | bnj769 34526 | . . . . . . 7 ⊢ (𝜒 → E Fr 𝑛) |
16 | 15 | bnj707 34519 | . . . . . 6 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → E Fr 𝑛) |
17 | bnj1030.10 | . . . . . . 7 ⊢ (𝜌 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜂)) | |
18 | bnj1030.17 | . . . . . . 7 ⊢ (𝜂′ ↔ [𝑗 / 𝑖]𝜂) | |
19 | bnj1030.18 | . . . . . . 7 ⊢ (𝜎 ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′)) | |
20 | bnj1030.19 | . . . . . . 7 ⊢ (𝜑0 ↔ (𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓)) | |
21 | 2, 8, 13, 18 | bnj1123 34750 | . . . . . . . . . 10 ⊢ (𝜂′ ↔ ((𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) → (𝑓‘𝑗) ⊆ 𝐵)) |
22 | 2, 3, 5, 7, 19, 20, 21 | bnj1118 34748 | . . . . . . . . 9 ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑓‘𝑖) ⊆ 𝐵) |
23 | 1, 3, 5 | bnj1097 34745 | . . . . . . . . 9 ⊢ ((𝑖 = ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑓‘𝑖) ⊆ 𝐵) |
24 | 22, 23 | bnj1109 34550 | . . . . . . . 8 ⊢ ∃𝑗(((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0) → (𝑓‘𝑖) ⊆ 𝐵) |
25 | 24, 2, 3 | bnj1093 34744 | . . . . . . 7 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵)) |
26 | 13, 17, 18, 19, 20, 25 | bnj1090 34743 | . . . . . 6 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖 ∈ 𝑛 (𝜌 → 𝜂)) |
27 | vex 3465 | . . . . . . 7 ⊢ 𝑛 ∈ V | |
28 | 27, 17 | bnj110 34622 | . . . . . 6 ⊢ (( E Fr 𝑛 ∧ ∀𝑖 ∈ 𝑛 (𝜌 → 𝜂)) → ∀𝑖 ∈ 𝑛 𝜂) |
29 | 16, 26, 28 | syl2anc 582 | . . . . 5 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖 ∈ 𝑛 𝜂) |
30 | 4, 5, 3, 6, 13, 29, 8 | bnj1121 34749 | . . . 4 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵) |
31 | 30 | gen2 1790 | . . 3 ⊢ ∀𝑛∀𝑖((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵) |
32 | 12, 31 | mpgbi 1792 | . 2 ⊢ (∃𝑓∃𝑛∃𝑖(𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵) |
33 | 1, 2, 3, 4, 5, 6, 7, 8, 32 | bnj1034 34734 | 1 ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1084 ∀wal 1531 = wceq 1533 ∃wex 1773 ∈ wcel 2098 {cab 2702 ∀wral 3050 ∃wrex 3059 Vcvv 3461 [wsbc 3773 ∖ cdif 3941 ⊆ wss 3944 ∅c0 4322 {csn 4630 ∪ ciun 4997 class class class wbr 5149 E cep 5581 Fr wfr 5630 dom cdm 5678 suc csuc 6373 Fn wfn 6544 ‘cfv 6549 ωcom 7871 ∧ w-bnj17 34450 predc-bnj14 34452 FrSe w-bnj15 34456 trClc-bnj18 34458 TrFow-bnj19 34460 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 ax-un 7741 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2930 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3964 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-iun 4999 df-br 5150 df-opab 5212 df-tr 5267 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-we 5635 df-ord 6374 df-on 6375 df-lim 6376 df-suc 6377 df-iota 6501 df-fn 6552 df-fv 6557 df-om 7872 df-bnj17 34451 df-bnj18 34459 df-bnj19 34461 |
This theorem is referenced by: bnj1124 34752 |
Copyright terms: Public domain | W3C validator |