![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > Mathboxes > strcollnfALT | GIF version |
Description: Alternate proof of strcollnf 15141, not using strcollnft 15140. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
strcollnf.nf | ⊢ Ⅎ𝑏𝜑 |
Ref | Expression |
---|---|
strcollnfALT | ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | strcoll2 15139 | . 2 ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑 ∧ ∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑)) | |
2 | nfcv 2332 | . . . . 5 ⊢ Ⅎ𝑏𝑎 | |
3 | nfcv 2332 | . . . . . 6 ⊢ Ⅎ𝑏𝑧 | |
4 | strcollnf.nf | . . . . . 6 ⊢ Ⅎ𝑏𝜑 | |
5 | 3, 4 | nfrexxy 2529 | . . . . 5 ⊢ Ⅎ𝑏∃𝑦 ∈ 𝑧 𝜑 |
6 | 2, 5 | nfralxy 2528 | . . . 4 ⊢ Ⅎ𝑏∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑 |
7 | 2, 4 | nfrexxy 2529 | . . . . 5 ⊢ Ⅎ𝑏∃𝑥 ∈ 𝑎 𝜑 |
8 | 3, 7 | nfralxy 2528 | . . . 4 ⊢ Ⅎ𝑏∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑 |
9 | 6, 8 | nfan 1576 | . . 3 ⊢ Ⅎ𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑 ∧ ∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑) |
10 | nfv 1539 | . . . 4 ⊢ Ⅎ𝑧∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 | |
11 | nfv 1539 | . . . 4 ⊢ Ⅎ𝑧∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑 | |
12 | 10, 11 | nfan 1576 | . . 3 ⊢ Ⅎ𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑) |
13 | rexeq 2687 | . . . . 5 ⊢ (𝑧 = 𝑏 → (∃𝑦 ∈ 𝑧 𝜑 ↔ ∃𝑦 ∈ 𝑏 𝜑)) | |
14 | 13 | ralbidv 2490 | . . . 4 ⊢ (𝑧 = 𝑏 → (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑 ↔ ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑)) |
15 | raleq 2686 | . . . 4 ⊢ (𝑧 = 𝑏 → (∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑 ↔ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)) | |
16 | 14, 15 | anbi12d 473 | . . 3 ⊢ (𝑧 = 𝑏 → ((∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑 ∧ ∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑) ↔ (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑))) |
17 | 9, 12, 16 | cbvex 1767 | . 2 ⊢ (∃𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑 ∧ ∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑) ↔ ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)) |
18 | 1, 17 | sylib 122 | 1 ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 Ⅎwnf 1471 ∃wex 1503 ∀wral 2468 ∃wrex 2469 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 ax-strcoll 15138 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 df-rex 2474 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |