Theorem strcollnft 16257

Description: Closed form of strcollnf 16258. (Contributed by BJ, 21-Oct-2019.)

Assertion

Ref	Expression
strcollnft	⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)))

Distinct variable group:   𝑎,𝑏,𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑎,𝑏)

Proof of Theorem strcollnft

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		strcoll2 16256	. 2 ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑 ∧ ∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑))
2		nfnf1 1570	. . . . 5 ⊢ Ⅎ𝑏Ⅎ𝑏𝜑
3	2	nfal 1602	. . . 4 ⊢ Ⅎ𝑏∀𝑦Ⅎ𝑏𝜑
4	3	nfal 1602	. . 3 ⊢ Ⅎ𝑏∀𝑥∀𝑦Ⅎ𝑏𝜑
5		nfa1 1567	. . . . 5 ⊢ Ⅎ𝑥∀𝑥∀𝑦Ⅎ𝑏𝜑
6		nfcvd 2353	. . . . 5 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏𝑎)
7		nfa1 1567	. . . . . . 7 ⊢ Ⅎ𝑦∀𝑦Ⅎ𝑏𝜑
8	7	nfal 1602	. . . . . 6 ⊢ Ⅎ𝑦∀𝑥∀𝑦Ⅎ𝑏𝜑
9		nfcvd 2353	. . . . . 6 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏𝑧)
10		sp 1537	. . . . . . 7 ⊢ (∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏𝜑)
11	10	sps 1563	. . . . . 6 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏𝜑)
12	8, 9, 11	nfrexdxy 2544	. . . . 5 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏∃𝑦 ∈ 𝑧 𝜑)
13	5, 6, 12	nfraldxy 2543	. . . 4 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑)
14	5, 6, 11	nfrexdxy 2544	. . . . 5 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏∃𝑥 ∈ 𝑎 𝜑)
15	8, 9, 14	nfraldxy 2543	. . . 4 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑)
16	13, 15	nfand 1594	. . 3 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑 ∧ ∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑))
17		nfv 1554	. . . . . . 7 ⊢ Ⅎ𝑥 𝑧 = 𝑏
18	5, 17	nfan 1591	. . . . . 6 ⊢ Ⅎ𝑥(∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏)
19		rexeq 2709	. . . . . . 7 ⊢ (𝑧 = 𝑏 → (∃𝑦 ∈ 𝑧 𝜑 ↔ ∃𝑦 ∈ 𝑏 𝜑))
20	19	adantl 277	. . . . . 6 ⊢ ((∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏) → (∃𝑦 ∈ 𝑧 𝜑 ↔ ∃𝑦 ∈ 𝑏 𝜑))
21	18, 20	ralbid 2508	. . . . 5 ⊢ ((∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏) → (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑 ↔ ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑))
22		nfv 1554	. . . . . . 7 ⊢ Ⅎ𝑦 𝑧 = 𝑏
23	8, 22	nfan 1591	. . . . . 6 ⊢ Ⅎ𝑦(∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏)
24		eleq2 2273	. . . . . . . 8 ⊢ (𝑧 = 𝑏 → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑏))
25	24	adantl 277	. . . . . . 7 ⊢ ((∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏) → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑏))
26	25	imbi1d 231	. . . . . 6 ⊢ ((∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏) → ((𝑦 ∈ 𝑧 → ∃𝑥 ∈ 𝑎 𝜑) ↔ (𝑦 ∈ 𝑏 → ∃𝑥 ∈ 𝑎 𝜑)))
27	23, 26	ralbid2 2514	. . . . 5 ⊢ ((∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏) → (∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑 ↔ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑))
28	21, 27	anbi12d 473	. . . 4 ⊢ ((∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏) → ((∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑 ∧ ∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑) ↔ (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)))
29	28	ex 115	. . 3 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → (𝑧 = 𝑏 → ((∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑 ∧ ∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑) ↔ (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑))))
30	4, 16, 29	cbvexd 1954	. 2 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → (∃𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑 ∧ ∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑) ↔ ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)))
31	1, 30	imbitrid 154	1 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1373  Ⅎwnf 1486  ∃wex 1518  ∀wral 2488  ∃wrex 2489

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191  ax-strcoll 16255

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ral 2493  df-rex 2494

This theorem is referenced by:  strcollnf  16258