Theorem strcollnft 17181

Description: Closed form of strcollnf 17182. (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 17180	. 2 ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑 ∧ ∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑))
2		nfnf1 1597	. . . . 5 ⊢ Ⅎ𝑏Ⅎ𝑏𝜑
3	2	nfal 1629	. . . 4 ⊢ Ⅎ𝑏∀𝑦Ⅎ𝑏𝜑
4	3	nfal 1629	. . 3 ⊢ Ⅎ𝑏∀𝑥∀𝑦Ⅎ𝑏𝜑
5		nfa1 1594	. . . . 5 ⊢ Ⅎ𝑥∀𝑥∀𝑦Ⅎ𝑏𝜑
6		nfcvd 2393	. . . . 5 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏𝑎)
7		nfa1 1594	. . . . . . 7 ⊢ Ⅎ𝑦∀𝑦Ⅎ𝑏𝜑
8	7	nfal 1629	. . . . . 6 ⊢ Ⅎ𝑦∀𝑥∀𝑦Ⅎ𝑏𝜑
9		nfcvd 2393	. . . . . 6 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏𝑧)
10		sp 1564	. . . . . . 7 ⊢ (∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏𝜑)
11	10	sps 1590	. . . . . 6 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏𝜑)
12	8, 9, 11	nfrexdxy 2584	. . . . 5 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏∃𝑦 ∈ 𝑧 𝜑)
13	5, 6, 12	nfraldxy 2583	. . . 4 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑)
14	5, 6, 11	nfrexdxy 2584	. . . . 5 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏∃𝑥 ∈ 𝑎 𝜑)
15	8, 9, 14	nfraldxy 2583	. . . 4 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑)
16	13, 15	nfand 1621	. . 3 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑 ∧ ∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑))
17		nfv 1581	. . . . . . 7 ⊢ Ⅎ𝑥 𝑧 = 𝑏
18	5, 17	nfan 1618	. . . . . 6 ⊢ Ⅎ𝑥(∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏)
19		rexeq 2750	. . . . . . 7 ⊢ (𝑧 = 𝑏 → (∃𝑦 ∈ 𝑧 𝜑 ↔ ∃𝑦 ∈ 𝑏 𝜑))
20	19	adantl 277	. . . . . 6 ⊢ ((∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏) → (∃𝑦 ∈ 𝑧 𝜑 ↔ ∃𝑦 ∈ 𝑏 𝜑))
21	18, 20	ralbid 2548	. . . . 5 ⊢ ((∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏) → (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑 ↔ ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑))
22		nfv 1581	. . . . . . 7 ⊢ Ⅎ𝑦 𝑧 = 𝑏
23	8, 22	nfan 1618	. . . . . 6 ⊢ Ⅎ𝑦(∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏)
24		eleq2 2302	. . . . . . . 8 ⊢ (𝑧 = 𝑏 → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑏))
25	24	adantl 277	. . . . . . 7 ⊢ ((∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏) → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑏))
26	25	imbi1d 231	. . . . . 6 ⊢ ((∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏) → ((𝑦 ∈ 𝑧 → ∃𝑥 ∈ 𝑎 𝜑) ↔ (𝑦 ∈ 𝑏 → ∃𝑥 ∈ 𝑎 𝜑)))
27	23, 26	ralbid2 2554	. . . . 5 ⊢ ((∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏) → (∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑 ↔ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑))
28	21, 27	anbi12d 477	. . . 4 ⊢ ((∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏) → ((∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑 ∧ ∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑) ↔ (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)))
29	28	ex 115	. . 3 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → (𝑧 = 𝑏 → ((∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑 ∧ ∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑) ↔ (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑))))
30	4, 16, 29	cbvexd 1983	. 2 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → (∃𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑧 𝜑 ∧ ∀𝑦 ∈ 𝑧 ∃𝑥 ∈ 𝑎 𝜑) ↔ ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)))
31	1, 30	imbitrid 154	1 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1400  Ⅎwnf 1513  ∃wex 1545  ∀wral 2528  ∃wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-strcoll 17179

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534

This theorem is used by:  strcollnf  17182