![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > Mathboxes > bj-inf2vnlem4 | GIF version |
Description: Lemma for bj-inf2vn2 12136. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
bj-inf2vnlem4 | ⊢ (∀𝑥 ∈ 𝐴 (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → (Ind 𝑍 → 𝐴 ⊆ 𝑍)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-inf2vnlem2 12132 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → (Ind 𝑍 → ∀𝑢(∀𝑡 ∈ 𝑢 (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) → (𝑢 ∈ 𝐴 → 𝑢 ∈ 𝑍)))) | |
2 | nfv 1467 | . . . 4 ⊢ Ⅎ𝑧(𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) | |
3 | nfv 1467 | . . . 4 ⊢ Ⅎ𝑧(𝑢 ∈ 𝐴 → 𝑢 ∈ 𝑍) | |
4 | nfv 1467 | . . . 4 ⊢ Ⅎ𝑢(𝑧 ∈ 𝐴 → 𝑧 ∈ 𝑍) | |
5 | nfv 1467 | . . . 4 ⊢ Ⅎ𝑢(𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) | |
6 | eleq1 2151 | . . . . . 6 ⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)) | |
7 | eleq1 2151 | . . . . . 6 ⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝑍 ↔ 𝑡 ∈ 𝑍)) | |
8 | 6, 7 | imbi12d 233 | . . . . 5 ⊢ (𝑧 = 𝑡 → ((𝑧 ∈ 𝐴 → 𝑧 ∈ 𝑍) ↔ (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍))) |
9 | 8 | biimpd 143 | . . . 4 ⊢ (𝑧 = 𝑡 → ((𝑧 ∈ 𝐴 → 𝑧 ∈ 𝑍) → (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍))) |
10 | eleq1 2151 | . . . . . 6 ⊢ (𝑧 = 𝑢 → (𝑧 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴)) | |
11 | eleq1 2151 | . . . . . 6 ⊢ (𝑧 = 𝑢 → (𝑧 ∈ 𝑍 ↔ 𝑢 ∈ 𝑍)) | |
12 | 10, 11 | imbi12d 233 | . . . . 5 ⊢ (𝑧 = 𝑢 → ((𝑧 ∈ 𝐴 → 𝑧 ∈ 𝑍) ↔ (𝑢 ∈ 𝐴 → 𝑢 ∈ 𝑍))) |
13 | 12 | biimprd 157 | . . . 4 ⊢ (𝑧 = 𝑢 → ((𝑢 ∈ 𝐴 → 𝑢 ∈ 𝑍) → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝑍))) |
14 | 2, 3, 4, 5, 9, 13 | setindis 12128 | . . 3 ⊢ (∀𝑢(∀𝑡 ∈ 𝑢 (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) → (𝑢 ∈ 𝐴 → 𝑢 ∈ 𝑍)) → ∀𝑧(𝑧 ∈ 𝐴 → 𝑧 ∈ 𝑍)) |
15 | 1, 14 | syl6 33 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → (Ind 𝑍 → ∀𝑧(𝑧 ∈ 𝐴 → 𝑧 ∈ 𝑍))) |
16 | dfss2 3015 | . 2 ⊢ (𝐴 ⊆ 𝑍 ↔ ∀𝑧(𝑧 ∈ 𝐴 → 𝑧 ∈ 𝑍)) | |
17 | 15, 16 | syl6ibr 161 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → (Ind 𝑍 → 𝐴 ⊆ 𝑍)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 665 ∀wal 1288 = wceq 1290 ∈ wcel 1439 ∀wral 2360 ∃wrex 2361 ⊆ wss 3000 ∅c0 3287 suc csuc 4201 Ind wind 12087 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 ax-setind 4366 |
This theorem depends on definitions: df-bi 116 df-tru 1293 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-ral 2365 df-rex 2366 df-v 2622 df-un 3004 df-in 3006 df-ss 3013 df-sn 3456 df-suc 4207 df-bj-ind 12088 |
This theorem is referenced by: bj-inf2vn2 12136 |
Copyright terms: Public domain | W3C validator |