Theorem fidcenumlemrks 6718

Description: Lemma for fidcenum 6721. Induction step for fidcenumlemrk 6719. (Contributed by Jim Kingdon, 20-Oct-2022.)

Hypotheses

Ref	Expression
fidcenumlemr.dc	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
fidcenumlemr.f	⊢ (𝜑 → 𝐹:𝑁–onto→𝐴)
fidcenumlemrks.j	⊢ (𝜑 → 𝐽 ∈ ω)
fidcenumlemrks.jn	⊢ (𝜑 → suc 𝐽 ⊆ 𝑁)
fidcenumlemrks.h	⊢ (𝜑 → (𝑋 ∈ (𝐹 “ 𝐽) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝐽)))
fidcenumlemrks.x	⊢ (𝜑 → 𝑋 ∈ 𝐴)

Assertion

Ref	Expression
fidcenumlemrks	⊢ (𝜑 → (𝑋 ∈ (𝐹 “ suc 𝐽) ∨ ¬ 𝑋 ∈ (𝐹 “ suc 𝐽)))

Distinct variable groups:   𝑥,𝐴,𝑦   𝑦,𝐹   𝑦,𝐽   𝑥,𝑋,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐹(𝑥)   𝐽(𝑥)   𝑁(𝑥,𝑦)

Proof of Theorem fidcenumlemrks

Step	Hyp	Ref	Expression
1		simpr 109	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝐹 “ 𝐽)) → 𝑋 ∈ (𝐹 “ 𝐽))
2		elun1 3170	. . . . 5 ⊢ (𝑋 ∈ (𝐹 “ 𝐽) → 𝑋 ∈ ((𝐹 “ 𝐽) ∪ (𝐹 “ {𝐽})))
3	1, 2	syl 14	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝐹 “ 𝐽)) → 𝑋 ∈ ((𝐹 “ 𝐽) ∪ (𝐹 “ {𝐽})))
4		df-suc 4209	. . . . . . 7 ⊢ suc 𝐽 = (𝐽 ∪ {𝐽})
5	4	imaeq2i 4787	. . . . . 6 ⊢ (𝐹 “ suc 𝐽) = (𝐹 “ (𝐽 ∪ {𝐽}))
6		imaundi 4859	. . . . . 6 ⊢ (𝐹 “ (𝐽 ∪ {𝐽})) = ((𝐹 “ 𝐽) ∪ (𝐹 “ {𝐽}))
7	5, 6	eqtri 2109	. . . . 5 ⊢ (𝐹 “ suc 𝐽) = ((𝐹 “ 𝐽) ∪ (𝐹 “ {𝐽}))
8	7	eleq2i 2155	. . . 4 ⊢ (𝑋 ∈ (𝐹 “ suc 𝐽) ↔ 𝑋 ∈ ((𝐹 “ 𝐽) ∪ (𝐹 “ {𝐽})))
9	3, 8	sylibr 133	. . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝐹 “ 𝐽)) → 𝑋 ∈ (𝐹 “ suc 𝐽))
10	9	orcd 688	. 2 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝐹 “ 𝐽)) → (𝑋 ∈ (𝐹 “ suc 𝐽) ∨ ¬ 𝑋 ∈ (𝐹 “ suc 𝐽)))
11		simpr 109	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝐹 “ 𝐽)) ∧ 𝑋 = (𝐹‘𝐽)) → 𝑋 = (𝐹‘𝐽))
12		fidcenumlemrks.x	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ 𝐴)
13		elsng 3467	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝐴 → (𝑋 ∈ {(𝐹‘𝐽)} ↔ 𝑋 = (𝐹‘𝐽)))
14	12, 13	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 ∈ {(𝐹‘𝐽)} ↔ 𝑋 = (𝐹‘𝐽)))
15		fidcenumlemr.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝑁–onto→𝐴)
16		fofn 5250	. . . . . . . . . . . 12 ⊢ (𝐹:𝑁–onto→𝐴 → 𝐹 Fn 𝑁)
17	15, 16	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 Fn 𝑁)
18		fidcenumlemrks.jn	. . . . . . . . . . . 12 ⊢ (𝜑 → suc 𝐽 ⊆ 𝑁)
19		fidcenumlemrks.j	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ ω)
20		sucidg 4254	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ ω → 𝐽 ∈ suc 𝐽)
21	19, 20	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ suc 𝐽)
22	18, 21	sseldd 3029	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 ∈ 𝑁)
23		fnsnfv 5378	. . . . . . . . . . 11 ⊢ ((𝐹 Fn 𝑁 ∧ 𝐽 ∈ 𝑁) → {(𝐹‘𝐽)} = (𝐹 “ {𝐽}))
24	17, 22, 23	syl2anc 404	. . . . . . . . . 10 ⊢ (𝜑 → {(𝐹‘𝐽)} = (𝐹 “ {𝐽}))
25	24	eleq2d 2158	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 ∈ {(𝐹‘𝐽)} ↔ 𝑋 ∈ (𝐹 “ {𝐽})))
26	14, 25	bitr3d 189	. . . . . . . 8 ⊢ (𝜑 → (𝑋 = (𝐹‘𝐽) ↔ 𝑋 ∈ (𝐹 “ {𝐽})))
27	26	ad2antrr 473	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝐹 “ 𝐽)) ∧ 𝑋 = (𝐹‘𝐽)) → (𝑋 = (𝐹‘𝐽) ↔ 𝑋 ∈ (𝐹 “ {𝐽})))
28	11, 27	mpbid 146	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝐹 “ 𝐽)) ∧ 𝑋 = (𝐹‘𝐽)) → 𝑋 ∈ (𝐹 “ {𝐽}))
29		elun2 3171	. . . . . 6 ⊢ (𝑋 ∈ (𝐹 “ {𝐽}) → 𝑋 ∈ ((𝐹 “ 𝐽) ∪ (𝐹 “ {𝐽})))
30	28, 29	syl 14	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝐹 “ 𝐽)) ∧ 𝑋 = (𝐹‘𝐽)) → 𝑋 ∈ ((𝐹 “ 𝐽) ∪ (𝐹 “ {𝐽})))
31	30, 8	sylibr 133	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝐹 “ 𝐽)) ∧ 𝑋 = (𝐹‘𝐽)) → 𝑋 ∈ (𝐹 “ suc 𝐽))
32	31	orcd 688	. . 3 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝐹 “ 𝐽)) ∧ 𝑋 = (𝐹‘𝐽)) → (𝑋 ∈ (𝐹 “ suc 𝐽) ∨ ¬ 𝑋 ∈ (𝐹 “ suc 𝐽)))
33		simplr 498	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝐹 “ 𝐽)) ∧ ¬ 𝑋 = (𝐹‘𝐽)) → ¬ 𝑋 ∈ (𝐹 “ 𝐽))
34		simpr 109	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝐹 “ 𝐽)) ∧ ¬ 𝑋 = (𝐹‘𝐽)) → ¬ 𝑋 = (𝐹‘𝐽))
35	26	ad2antrr 473	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝐹 “ 𝐽)) ∧ ¬ 𝑋 = (𝐹‘𝐽)) → (𝑋 = (𝐹‘𝐽) ↔ 𝑋 ∈ (𝐹 “ {𝐽})))
36	34, 35	mtbid 633	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝐹 “ 𝐽)) ∧ ¬ 𝑋 = (𝐹‘𝐽)) → ¬ 𝑋 ∈ (𝐹 “ {𝐽}))
37		ioran 705	. . . . . . 7 ⊢ (¬ (𝑋 ∈ (𝐹 “ 𝐽) ∨ 𝑋 ∈ (𝐹 “ {𝐽})) ↔ (¬ 𝑋 ∈ (𝐹 “ 𝐽) ∧ ¬ 𝑋 ∈ (𝐹 “ {𝐽})))
38	33, 36, 37	sylanbrc 409	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝐹 “ 𝐽)) ∧ ¬ 𝑋 = (𝐹‘𝐽)) → ¬ (𝑋 ∈ (𝐹 “ 𝐽) ∨ 𝑋 ∈ (𝐹 “ {𝐽})))
39		elun 3144	. . . . . 6 ⊢ (𝑋 ∈ ((𝐹 “ 𝐽) ∪ (𝐹 “ {𝐽})) ↔ (𝑋 ∈ (𝐹 “ 𝐽) ∨ 𝑋 ∈ (𝐹 “ {𝐽})))
40	38, 39	sylnibr 638	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝐹 “ 𝐽)) ∧ ¬ 𝑋 = (𝐹‘𝐽)) → ¬ 𝑋 ∈ ((𝐹 “ 𝐽) ∪ (𝐹 “ {𝐽})))
41	40, 8	sylnibr 638	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝐹 “ 𝐽)) ∧ ¬ 𝑋 = (𝐹‘𝐽)) → ¬ 𝑋 ∈ (𝐹 “ suc 𝐽))
42	41	olcd 689	. . 3 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝐹 “ 𝐽)) ∧ ¬ 𝑋 = (𝐹‘𝐽)) → (𝑋 ∈ (𝐹 “ suc 𝐽) ∨ ¬ 𝑋 ∈ (𝐹 “ suc 𝐽)))
43		fof 5248	. . . . . . . 8 ⊢ (𝐹:𝑁–onto→𝐴 → 𝐹:𝑁⟶𝐴)
44	15, 43	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝑁⟶𝐴)
45	44, 22	ffvelrnd 5451	. . . . . 6 ⊢ (𝜑 → (𝐹‘𝐽) ∈ 𝐴)
46		fidcenumlemr.dc	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
47		eqeq1 2095	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝑥 = 𝑦 ↔ 𝑋 = 𝑦))
48	47	dcbid 787	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (DECID 𝑥 = 𝑦 ↔ DECID 𝑋 = 𝑦))
49		eqeq2 2098	. . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝐽) → (𝑋 = 𝑦 ↔ 𝑋 = (𝐹‘𝐽)))
50	49	dcbid 787	. . . . . . 7 ⊢ (𝑦 = (𝐹‘𝐽) → (DECID 𝑋 = 𝑦 ↔ DECID 𝑋 = (𝐹‘𝐽)))
51	48, 50	rspc2va 2738	. . . . . 6 ⊢ (((𝑋 ∈ 𝐴 ∧ (𝐹‘𝐽) ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) → DECID 𝑋 = (𝐹‘𝐽))
52	12, 45, 46, 51	syl21anc 1174	. . . . 5 ⊢ (𝜑 → DECID 𝑋 = (𝐹‘𝐽))
53		exmiddc 783	. . . . 5 ⊢ (DECID 𝑋 = (𝐹‘𝐽) → (𝑋 = (𝐹‘𝐽) ∨ ¬ 𝑋 = (𝐹‘𝐽)))
54	52, 53	syl 14	. . . 4 ⊢ (𝜑 → (𝑋 = (𝐹‘𝐽) ∨ ¬ 𝑋 = (𝐹‘𝐽)))
55	54	adantr 271	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑋 ∈ (𝐹 “ 𝐽)) → (𝑋 = (𝐹‘𝐽) ∨ ¬ 𝑋 = (𝐹‘𝐽)))
56	32, 42, 55	mpjaodan 748	. 2 ⊢ ((𝜑 ∧ ¬ 𝑋 ∈ (𝐹 “ 𝐽)) → (𝑋 ∈ (𝐹 “ suc 𝐽) ∨ ¬ 𝑋 ∈ (𝐹 “ suc 𝐽)))
57		fidcenumlemrks.h	. 2 ⊢ (𝜑 → (𝑋 ∈ (𝐹 “ 𝐽) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝐽)))
58	10, 56, 57	mpjaodan 748	1 ⊢ (𝜑 → (𝑋 ∈ (𝐹 “ suc 𝐽) ∨ ¬ 𝑋 ∈ (𝐹 “ suc 𝐽)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 665  DECID wdc 781   = wceq 1290   ∈ wcel 1439  ∀wral 2360   ∪ cun 3000   ⊆ wss 3002  {csn 3452  suc csuc 4203  ωcom 4420   “ cima 4457   Fn wfn 5025  ⟶wf 5026  –onto→wfo 5028  ‘cfv 5030

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3965  ax-pow 4017  ax-pr 4047

This theorem depends on definitions:  df-bi 116  df-dc 782  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ral 2365  df-rex 2366  df-v 2624  df-sbc 2844  df-un 3006  df-in 3008  df-ss 3015  df-pw 3437  df-sn 3458  df-pr 3459  df-op 3461  df-uni 3662  df-br 3854  df-opab 3908  df-id 4131  df-suc 4209  df-xp 4460  df-rel 4461  df-cnv 4462  df-co 4463  df-dm 4464  df-rn 4465  df-res 4466  df-ima 4467  df-iota 4995  df-fun 5032  df-fn 5033  df-f 5034  df-fo 5036  df-fv 5038

This theorem is referenced by:  fidcenumlemrk  6719