Theorem sscoll2 13186

Description: Version of ax-sscoll 13185 with two disjoint variable conditions removed and without initial universal quantifiers. (Contributed by BJ, 5-Oct-2019.)

Assertion

Ref	Expression
sscoll2	⊢ ∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑))

Distinct variable groups:   𝑎,𝑏,𝑐,𝑑,𝑥,𝑦,𝑧   𝜑,𝑐,𝑑

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

Proof of Theorem sscoll2

Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1508	. . 3 ⊢ Ⅎ𝑐(𝑢 = 𝑎 ∧ 𝑣 = 𝑏)
2		nfv 1508	. . . 4 ⊢ Ⅎ𝑧(𝑢 = 𝑎 ∧ 𝑣 = 𝑏)
3		simpl 108	. . . . . 6 ⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → 𝑢 = 𝑎)
4		rexeq 2627	. . . . . . 7 ⊢ (𝑣 = 𝑏 → (∃𝑦 ∈ 𝑣 𝜑 ↔ ∃𝑦 ∈ 𝑏 𝜑))
5	4	adantl 275	. . . . . 6 ⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∃𝑦 ∈ 𝑣 𝜑 ↔ ∃𝑦 ∈ 𝑏 𝜑))
6	3, 5	raleqbidv 2638	. . . . 5 ⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 ↔ ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑))
7		nfv 1508	. . . . . 6 ⊢ Ⅎ𝑑(𝑢 = 𝑎 ∧ 𝑣 = 𝑏)
8		nfv 1508	. . . . . . 7 ⊢ Ⅎ𝑦(𝑢 = 𝑎 ∧ 𝑣 = 𝑏)
9		rexeq 2627	. . . . . . . . 9 ⊢ (𝑢 = 𝑎 → (∃𝑥 ∈ 𝑢 𝜑 ↔ ∃𝑥 ∈ 𝑎 𝜑))
10	9	adantr 274	. . . . . . . 8 ⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∃𝑥 ∈ 𝑢 𝜑 ↔ ∃𝑥 ∈ 𝑎 𝜑))
11	10	bibi2d 231	. . . . . . 7 ⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → ((𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑) ↔ (𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)))
12	8, 11	albid 1594	. . . . . 6 ⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)))
13	7, 12	rexbid 2436	. . . . 5 ⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑) ↔ ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)))
14	6, 13	imbi12d 233	. . . 4 ⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑)) ↔ (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑))))
15	2, 14	albid 1594	. . 3 ⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∀𝑧(∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑)) ↔ ∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑))))
16	1, 15	exbid 1595	. 2 ⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∃𝑐∀𝑧(∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑)) ↔ ∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑))))
17		ax-sscoll 13185	. . . 4 ⊢ ∀𝑢∀𝑣∃𝑐∀𝑧(∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑))
18	17	spi 1516	. . 3 ⊢ ∀𝑣∃𝑐∀𝑧(∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑))
19	18	spi 1516	. 2 ⊢ ∃𝑐∀𝑧(∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑))
20	16, 19	ch2varv 12975	1 ⊢ ∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1329  ∃wex 1468  ∀wral 2416  ∃wrex 2417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sscoll 13185

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422

This theorem is referenced by: (None)