Theorem ssfiexmid 6254

Description: If any subset of a finite set is finite, excluded middle follows. One direction of Theorem 2.1 of [Bauer], p. 485. (Contributed by Jim Kingdon, 19-May-2020.)

Hypothesis

Ref	Expression
ssfiexmid.1	⊢ ∀x∀y((x ∈ Fin ∧ y ⊆ x) → y ∈ Fin)

Assertion

Ref	Expression
ssfiexmid	⊢ (φ ∨ ¬ φ)

Distinct variable group:   φ,x,y

Proof of Theorem ssfiexmid

Dummy variables 𝑛 z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0ex 3875	. . . . 5 ⊢ ∅ ∈ V
2		snfig 6227	. . . . 5 ⊢ (∅ ∈ V → {∅} ∈ Fin)
3	1, 2	ax-mp 7	. . . 4 ⊢ {∅} ∈ Fin
4		ssrab2 3019	. . . 4 ⊢ {z ∈ {∅} ∣ φ} ⊆ {∅}
5		ssfiexmid.1	. . . . . 6 ⊢ ∀x∀y((x ∈ Fin ∧ y ⊆ x) → y ∈ Fin)
6		p0ex 3930	. . . . . . 7 ⊢ {∅} ∈ V
7		eleq1 2097	. . . . . . . . . 10 ⊢ (x = {∅} → (x ∈ Fin ↔ {∅} ∈ Fin))
8		sseq2 2961	. . . . . . . . . 10 ⊢ (x = {∅} → (y ⊆ x ↔ y ⊆ {∅}))
9	7, 8	anbi12d 442	. . . . . . . . 9 ⊢ (x = {∅} → ((x ∈ Fin ∧ y ⊆ x) ↔ ({∅} ∈ Fin ∧ y ⊆ {∅})))
10	9	imbi1d 220	. . . . . . . 8 ⊢ (x = {∅} → (((x ∈ Fin ∧ y ⊆ x) → y ∈ Fin) ↔ (({∅} ∈ Fin ∧ y ⊆ {∅}) → y ∈ Fin)))
11	10	albidv 1702	. . . . . . 7 ⊢ (x = {∅} → (∀y((x ∈ Fin ∧ y ⊆ x) → y ∈ Fin) ↔ ∀y(({∅} ∈ Fin ∧ y ⊆ {∅}) → y ∈ Fin)))
12	6, 11	spcv 2640	. . . . . 6 ⊢ (∀x∀y((x ∈ Fin ∧ y ⊆ x) → y ∈ Fin) → ∀y(({∅} ∈ Fin ∧ y ⊆ {∅}) → y ∈ Fin))
13	5, 12	ax-mp 7	. . . . 5 ⊢ ∀y(({∅} ∈ Fin ∧ y ⊆ {∅}) → y ∈ Fin)
14	6	rabex 3892	. . . . . 6 ⊢ {z ∈ {∅} ∣ φ} ∈ V
15		sseq1 2960	. . . . . . . 8 ⊢ (y = {z ∈ {∅} ∣ φ} → (y ⊆ {∅} ↔ {z ∈ {∅} ∣ φ} ⊆ {∅}))
16	15	anbi2d 437	. . . . . . 7 ⊢ (y = {z ∈ {∅} ∣ φ} → (({∅} ∈ Fin ∧ y ⊆ {∅}) ↔ ({∅} ∈ Fin ∧ {z ∈ {∅} ∣ φ} ⊆ {∅})))
17		eleq1 2097	. . . . . . 7 ⊢ (y = {z ∈ {∅} ∣ φ} → (y ∈ Fin ↔ {z ∈ {∅} ∣ φ} ∈ Fin))
18	16, 17	imbi12d 223	. . . . . 6 ⊢ (y = {z ∈ {∅} ∣ φ} → ((({∅} ∈ Fin ∧ y ⊆ {∅}) → y ∈ Fin) ↔ (({∅} ∈ Fin ∧ {z ∈ {∅} ∣ φ} ⊆ {∅}) → {z ∈ {∅} ∣ φ} ∈ Fin)))
19	14, 18	spcv 2640	. . . . 5 ⊢ (∀y(({∅} ∈ Fin ∧ y ⊆ {∅}) → y ∈ Fin) → (({∅} ∈ Fin ∧ {z ∈ {∅} ∣ φ} ⊆ {∅}) → {z ∈ {∅} ∣ φ} ∈ Fin))
20	13, 19	ax-mp 7	. . . 4 ⊢ (({∅} ∈ Fin ∧ {z ∈ {∅} ∣ φ} ⊆ {∅}) → {z ∈ {∅} ∣ φ} ∈ Fin)
21	3, 4, 20	mp2an 402	. . 3 ⊢ {z ∈ {∅} ∣ φ} ∈ Fin
22		isfi 6177	. . 3 ⊢ ({z ∈ {∅} ∣ φ} ∈ Fin ↔ ∃𝑛 ∈ 𝜔 {z ∈ {∅} ∣ φ} ≈ 𝑛)
23	21, 22	mpbi 133	. 2 ⊢ ∃𝑛 ∈ 𝜔 {z ∈ {∅} ∣ φ} ≈ 𝑛
24		0elnn 4283	. . . . 5 ⊢ (𝑛 ∈ 𝜔 → (𝑛 = ∅ ∨ ∅ ∈ 𝑛))
25		breq2 3759	. . . . . . . . . 10 ⊢ (𝑛 = ∅ → ({z ∈ {∅} ∣ φ} ≈ 𝑛 ↔ {z ∈ {∅} ∣ φ} ≈ ∅))
26		en0 6211	. . . . . . . . . 10 ⊢ ({z ∈ {∅} ∣ φ} ≈ ∅ ↔ {z ∈ {∅} ∣ φ} = ∅)
27	25, 26	syl6bb 185	. . . . . . . . 9 ⊢ (𝑛 = ∅ → ({z ∈ {∅} ∣ φ} ≈ 𝑛 ↔ {z ∈ {∅} ∣ φ} = ∅))
28	27	biimpac 282	. . . . . . . 8 ⊢ (({z ∈ {∅} ∣ φ} ≈ 𝑛 ∧ 𝑛 = ∅) → {z ∈ {∅} ∣ φ} = ∅)
29		rabeq0 3241	. . . . . . . . 9 ⊢ ({z ∈ {∅} ∣ φ} = ∅ ↔ ∀z ∈ {∅} ¬ φ)
30	1	snm 3479	. . . . . . . . . 10 ⊢ ∃w w ∈ {∅}
31		r19.3rmv 3306	. . . . . . . . . 10 ⊢ (∃w w ∈ {∅} → (¬ φ ↔ ∀z ∈ {∅} ¬ φ))
32	30, 31	ax-mp 7	. . . . . . . . 9 ⊢ (¬ φ ↔ ∀z ∈ {∅} ¬ φ)
33	29, 32	bitr4i 176	. . . . . . . 8 ⊢ ({z ∈ {∅} ∣ φ} = ∅ ↔ ¬ φ)
34	28, 33	sylib 127	. . . . . . 7 ⊢ (({z ∈ {∅} ∣ φ} ≈ 𝑛 ∧ 𝑛 = ∅) → ¬ φ)
35	34	olcd 652	. . . . . 6 ⊢ (({z ∈ {∅} ∣ φ} ≈ 𝑛 ∧ 𝑛 = ∅) → (φ ∨ ¬ φ))
36		ensym 6197	. . . . . . . 8 ⊢ ({z ∈ {∅} ∣ φ} ≈ 𝑛 → 𝑛 ≈ {z ∈ {∅} ∣ φ})
37		elex2 2564	. . . . . . . 8 ⊢ (∅ ∈ 𝑛 → ∃x x ∈ 𝑛)
38		enm 6230	. . . . . . . 8 ⊢ ((𝑛 ≈ {z ∈ {∅} ∣ φ} ∧ ∃x x ∈ 𝑛) → ∃y y ∈ {z ∈ {∅} ∣ φ})
39	36, 37, 38	syl2an 273	. . . . . . 7 ⊢ (({z ∈ {∅} ∣ φ} ≈ 𝑛 ∧ ∅ ∈ 𝑛) → ∃y y ∈ {z ∈ {∅} ∣ φ})
40		biidd 161	. . . . . . . . . . 11 ⊢ (z = y → (φ ↔ φ))
41	40	elrab 2692	. . . . . . . . . 10 ⊢ (y ∈ {z ∈ {∅} ∣ φ} ↔ (y ∈ {∅} ∧ φ))
42	41	simprbi 260	. . . . . . . . 9 ⊢ (y ∈ {z ∈ {∅} ∣ φ} → φ)
43	42	orcd 651	. . . . . . . 8 ⊢ (y ∈ {z ∈ {∅} ∣ φ} → (φ ∨ ¬ φ))
44	43	exlimiv 1486	. . . . . . 7 ⊢ (∃y y ∈ {z ∈ {∅} ∣ φ} → (φ ∨ ¬ φ))
45	39, 44	syl 14	. . . . . 6 ⊢ (({z ∈ {∅} ∣ φ} ≈ 𝑛 ∧ ∅ ∈ 𝑛) → (φ ∨ ¬ φ))
46	35, 45	jaodan 709	. . . . 5 ⊢ (({z ∈ {∅} ∣ φ} ≈ 𝑛 ∧ (𝑛 = ∅ ∨ ∅ ∈ 𝑛)) → (φ ∨ ¬ φ))
47	24, 46	sylan2 270	. . . 4 ⊢ (({z ∈ {∅} ∣ φ} ≈ 𝑛 ∧ 𝑛 ∈ 𝜔) → (φ ∨ ¬ φ))
48	47	ancoms 255	. . 3 ⊢ ((𝑛 ∈ 𝜔 ∧ {z ∈ {∅} ∣ φ} ≈ 𝑛) → (φ ∨ ¬ φ))
49	48	rexlimiva 2422	. 2 ⊢ (∃𝑛 ∈ 𝜔 {z ∈ {∅} ∣ φ} ≈ 𝑛 → (φ ∨ ¬ φ))
50	23, 49	ax-mp 7	1 ⊢ (φ ∨ ¬ φ)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 628  ∀wal 1240   = wceq 1242  ∃wex 1378   ∈ wcel 1390  ∀wral 2300  ∃wrex 2301  {crab 2304  Vcvv 2551   ⊆ wss 2911  ∅c0 3218  {csn 3367   class class class wbr 3755  𝜔com 4256   ≈ cen 6155  Fincfn 6157

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-nul 3874  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-iinf 4254

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-sbc 2759  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-br 3756  df-opab 3810  df-id 4021  df-suc 4074  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-1o 5940  df-er 6042  df-en 6158  df-fin 6160

This theorem is referenced by: (None)