Theorem fin23lem26 10339

Description: Lemma for fin23lem22 10341. (Contributed by Stefan O'Rear, 1-Nov-2014.)

Assertion

Ref	Expression
fin23lem26	⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖)

Distinct variable group:   𝑖,𝑗,𝑆

Proof of Theorem fin23lem26

Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 5123	. . . 4 ⊢ (𝑖 = ∅ → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ ∅))
2	1	rexbidv 3164	. . 3 ⊢ (𝑖 = ∅ → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ ∅))
3		breq2 5123	. . . 4 ⊢ (𝑖 = 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ 𝑎))
4	3	rexbidv 3164	. . 3 ⊢ (𝑖 = 𝑎 → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎))
5		breq2 5123	. . . 4 ⊢ (𝑖 = suc 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ suc 𝑎))
6	5	rexbidv 3164	. . 3 ⊢ (𝑖 = suc 𝑎 → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎))
7		ordom 7871	. . . . 5 ⊢ Ord ω
8		simpl 482	. . . . 5 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ⊆ ω)
9		0fi 9056	. . . . . . . 8 ⊢ ∅ ∈ Fin
10		eleq1 2822	. . . . . . . 8 ⊢ (𝑆 = ∅ → (𝑆 ∈ Fin ↔ ∅ ∈ Fin))
11	9, 10	mpbiri 258	. . . . . . 7 ⊢ (𝑆 = ∅ → 𝑆 ∈ Fin)
12	11	necon3bi 2958	. . . . . 6 ⊢ (¬ 𝑆 ∈ Fin → 𝑆 ≠ ∅)
13	12	adantl 481	. . . . 5 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ≠ ∅)
14		tz7.5 6373	. . . . 5 ⊢ ((Ord ω ∧ 𝑆 ⊆ ω ∧ 𝑆 ≠ ∅) → ∃𝑗 ∈ 𝑆 (𝑆 ∩ 𝑗) = ∅)
15	7, 8, 13, 14	mp3an2i 1468	. . . 4 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗 ∈ 𝑆 (𝑆 ∩ 𝑗) = ∅)
16		en0 9032	. . . . . 6 ⊢ ((𝑗 ∩ 𝑆) ≈ ∅ ↔ (𝑗 ∩ 𝑆) = ∅)
17		incom 4184	. . . . . . 7 ⊢ (𝑗 ∩ 𝑆) = (𝑆 ∩ 𝑗)
18	17	eqeq1i 2740	. . . . . 6 ⊢ ((𝑗 ∩ 𝑆) = ∅ ↔ (𝑆 ∩ 𝑗) = ∅)
19	16, 18	bitri 275	. . . . 5 ⊢ ((𝑗 ∩ 𝑆) ≈ ∅ ↔ (𝑆 ∩ 𝑗) = ∅)
20	19	rexbii 3083	. . . 4 ⊢ (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ ∅ ↔ ∃𝑗 ∈ 𝑆 (𝑆 ∩ 𝑗) = ∅)
21	15, 20	sylibr 234	. . 3 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ ∅)
22		simplrl 776	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑆 ⊆ ω)
23		omsson 7865	. . . . . . . . . . 11 ⊢ ω ⊆ On
24	22, 23	sstrdi 3971	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑆 ⊆ On)
25	24	ssdifssd 4122	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ⊆ On)
26		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → ¬ 𝑆 ∈ Fin)
27		ssel2 3953	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ ω ∧ 𝑗 ∈ 𝑆) → 𝑗 ∈ ω)
28		onfin2 9240	. . . . . . . . . . . . . . . . 17 ⊢ ω = (On ∩ Fin)
29		inss2 4213	. . . . . . . . . . . . . . . . 17 ⊢ (On ∩ Fin) ⊆ Fin
30	28, 29	eqsstri 4005	. . . . . . . . . . . . . . . 16 ⊢ ω ⊆ Fin
31		peano2 7886	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ω → suc 𝑗 ∈ ω)
32	30, 31	sselid 3956	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ω → suc 𝑗 ∈ Fin)
33	27, 32	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ⊆ ω ∧ 𝑗 ∈ 𝑆) → suc 𝑗 ∈ Fin)
34	33	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → suc 𝑗 ∈ Fin)
35		ssfi 9187	. . . . . . . . . . . . . 14 ⊢ ((suc 𝑗 ∈ Fin ∧ 𝑆 ⊆ suc 𝑗) → 𝑆 ∈ Fin)
36	35	ex 412	. . . . . . . . . . . . 13 ⊢ (suc 𝑗 ∈ Fin → (𝑆 ⊆ suc 𝑗 → 𝑆 ∈ Fin))
37	34, 36	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → (𝑆 ⊆ suc 𝑗 → 𝑆 ∈ Fin))
38	26, 37	mtod 198	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → ¬ 𝑆 ⊆ suc 𝑗)
39		ssdif0 4341	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) = ∅)
40	39	necon3bbii 2979	. . . . . . . . . . 11 ⊢ (¬ 𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) ≠ ∅)
41	38, 40	sylib 218	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → (𝑆 ∖ suc 𝑗) ≠ ∅)
42	41	ad2ant2lr 748	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ≠ ∅)
43		onint 7784	. . . . . . . . 9 ⊢ (((𝑆 ∖ suc 𝑗) ⊆ On ∧ (𝑆 ∖ suc 𝑗) ≠ ∅) → ∩ (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
44	25, 42, 43	syl2anc 584	. . . . . . . 8 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∩ (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
45	44	eldifad 3938	. . . . . . 7 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∩ (𝑆 ∖ suc 𝑗) ∈ 𝑆)
46		simprr 772	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑗 ∩ 𝑆) ≈ 𝑎)
47		en2sn 9055	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ V ∧ 𝑎 ∈ V) → {𝑗} ≈ {𝑎})
48	47	el2v 3466	. . . . . . . . . 10 ⊢ {𝑗} ≈ {𝑎}
49	48	a1i 11	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → {𝑗} ≈ {𝑎})
50		simprl 770	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑗 ∈ 𝑆)
51	22, 50	sseldd 3959	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑗 ∈ ω)
52		nnord 7869	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ω → Ord 𝑗)
53	51, 52	syl 17	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → Ord 𝑗)
54		ordirr 6370	. . . . . . . . . . . 12 ⊢ (Ord 𝑗 → ¬ 𝑗 ∈ 𝑗)
55		elinel1 4176	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (𝑗 ∩ 𝑆) → 𝑗 ∈ 𝑗)
56	54, 55	nsyl 140	. . . . . . . . . . 11 ⊢ (Ord 𝑗 → ¬ 𝑗 ∈ (𝑗 ∩ 𝑆))
57		disjsn 4687	. . . . . . . . . . 11 ⊢ (((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅ ↔ ¬ 𝑗 ∈ (𝑗 ∩ 𝑆))
58	56, 57	sylibr 234	. . . . . . . . . 10 ⊢ (Ord 𝑗 → ((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅)
59	53, 58	syl 17	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅)
60		nnord 7869	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ω → Ord 𝑎)
61		ordirr 6370	. . . . . . . . . . . 12 ⊢ (Ord 𝑎 → ¬ 𝑎 ∈ 𝑎)
62	60, 61	syl 17	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ω → ¬ 𝑎 ∈ 𝑎)
63		disjsn 4687	. . . . . . . . . . 11 ⊢ ((𝑎 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ 𝑎)
64	62, 63	sylibr 234	. . . . . . . . . 10 ⊢ (𝑎 ∈ ω → (𝑎 ∩ {𝑎}) = ∅)
65	64	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑎 ∩ {𝑎}) = ∅)
66		unen 9060	. . . . . . . . 9 ⊢ ((((𝑗 ∩ 𝑆) ≈ 𝑎 ∧ {𝑗} ≈ {𝑎}) ∧ (((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅ ∧ (𝑎 ∩ {𝑎}) = ∅)) → ((𝑗 ∩ 𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎}))
67	46, 49, 59, 65, 66	syl22anc 838	. . . . . . . 8 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎}))
68		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → 𝑏 ∈ 𝑆)
69		simplrl 776	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → 𝑆 ⊆ ω)
70	69, 23	sstrdi 3971	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → 𝑆 ⊆ On)
71		ordsuc 7807	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord 𝑗 ↔ Ord suc 𝑗)
72	53, 71	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → Ord suc 𝑗)
73	72	adantrr 717	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → Ord suc 𝑗)
74		simp2 1137	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → 𝑆 ⊆ On)
75	74	ssdifssd 4122	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ On)
76		simpl1 1192	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ 𝑆)
77		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → ¬ 𝑏 ∈ suc 𝑗)
78	76, 77	eldifd 3937	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ (𝑆 ∖ suc 𝑗))
79	78	ex 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗 → 𝑏 ∈ (𝑆 ∖ suc 𝑗)))
80		onnmin 7792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ∖ suc 𝑗) ⊆ On ∧ 𝑏 ∈ (𝑆 ∖ suc 𝑗)) → ¬ 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗))
81	75, 79, 80	syl6an 684	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗 → ¬ 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗)))
82	81	con4d 115	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) → 𝑏 ∈ suc 𝑗))
83	82	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗)) → 𝑏 ∈ suc 𝑗)
84		simp3 1138	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → Ord suc 𝑗)
85		ordsucss 7812	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Ord suc 𝑗 → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗))
86	84, 85	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗))
87	86	imp 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → suc 𝑏 ⊆ suc 𝑗)
88	87	sscond 4121	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏))
89		intss 4945	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏) → ∩ (𝑆 ∖ suc 𝑏) ⊆ ∩ (𝑆 ∖ suc 𝑗))
90	88, 89	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → ∩ (𝑆 ∖ suc 𝑏) ⊆ ∩ (𝑆 ∖ suc 𝑗))
91		simpl2 1193	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑆 ⊆ On)
92		ordelon 6376	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Ord suc 𝑗 ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
93	84, 92	sylan 580	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
94		onmindif 6446	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ⊆ On ∧ 𝑏 ∈ On) → 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑏))
95	91, 93, 94	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑏))
96	90, 95	sseldd 3959	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗))
97	83, 96	impbida 800	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗))
98	68, 70, 73, 97	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗))
99		df-suc 6358	. . . . . . . . . . . . . . . 16 ⊢ suc 𝑗 = (𝑗 ∪ {𝑗})
100	99	eleq2i 2826	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ suc 𝑗 ↔ 𝑏 ∈ (𝑗 ∪ {𝑗}))
101	98, 100	bitrdi 287	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗})))
102	101	expr 456	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑏 ∈ 𝑆 → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗}))))
103	102	pm5.32rd 578	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ∧ 𝑏 ∈ 𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏 ∈ 𝑆)))
104		elin 3942	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ∧ 𝑏 ∈ 𝑆))
105		elin 3942	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏 ∈ 𝑆))
106	103, 104, 105	3bitr4g 314	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑏 ∈ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ 𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆)))
107	106	eqrdv 2733	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∪ {𝑗}) ∩ 𝑆))
108		indir 4261	. . . . . . . . . 10 ⊢ ((𝑗 ∪ {𝑗}) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆))
109	107, 108	eqtrdi 2786	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)))
110		snssi 4784	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ 𝑆 → {𝑗} ⊆ 𝑆)
111		dfss2 3944	. . . . . . . . . . . 12 ⊢ ({𝑗} ⊆ 𝑆 ↔ ({𝑗} ∩ 𝑆) = {𝑗})
112	110, 111	sylib 218	. . . . . . . . . . 11 ⊢ (𝑗 ∈ 𝑆 → ({𝑗} ∩ 𝑆) = {𝑗})
113	112	uneq2d 4143	. . . . . . . . . 10 ⊢ (𝑗 ∈ 𝑆 → ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗 ∩ 𝑆) ∪ {𝑗}))
114	113	ad2antrl 728	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗 ∩ 𝑆) ∪ {𝑗}))
115	109, 114	eqtrd 2770	. . . . . . . 8 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ {𝑗}))
116		df-suc 6358	. . . . . . . . 9 ⊢ suc 𝑎 = (𝑎 ∪ {𝑎})
117	116	a1i 11	. . . . . . . 8 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → suc 𝑎 = (𝑎 ∪ {𝑎}))
118	67, 115, 117	3brtr4d 5151	. . . . . . 7 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎)
119		ineq1 4188	. . . . . . . . 9 ⊢ (𝑏 = ∩ (𝑆 ∖ suc 𝑗) → (𝑏 ∩ 𝑆) = (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆))
120	119	breq1d 5129	. . . . . . . 8 ⊢ (𝑏 = ∩ (𝑆 ∖ suc 𝑗) → ((𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎))
121	120	rspcev 3601	. . . . . . 7 ⊢ ((∩ (𝑆 ∖ suc 𝑗) ∈ 𝑆 ∧ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎) → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎)
122	45, 118, 121	syl2anc 584	. . . . . 6 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎)
123	122	rexlimdvaa 3142	. . . . 5 ⊢ ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎))
124		ineq1 4188	. . . . . . 7 ⊢ (𝑏 = 𝑗 → (𝑏 ∩ 𝑆) = (𝑗 ∩ 𝑆))
125	124	breq1d 5129	. . . . . 6 ⊢ (𝑏 = 𝑗 → ((𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ (𝑗 ∩ 𝑆) ≈ suc 𝑎))
126	125	cbvrexvw 3221	. . . . 5 ⊢ (∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎)
127	123, 126	imbitrdi 251	. . . 4 ⊢ ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎))
128	127	ex 412	. . 3 ⊢ (𝑎 ∈ ω → ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎)))
129	2, 4, 6, 21, 128	finds2 7894	. 2 ⊢ (𝑖 ∈ ω → ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖))
130	129	impcom 407	1 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108   ≠ wne 2932  ∃wrex 3060  Vcvv 3459   ∖ cdif 3923   ∪ cun 3924   ∩ cin 3925   ⊆ wss 3926  ∅c0 4308  {csn 4601  ∩ cint 4922   class class class wbr 5119  Ord word 6351  Oncon0 6352  suc csuc 6354  ωcom 7861   ≈ cen 8956  Fincfn 8959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-int 4923  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-om 7862  df-1o 8480  df-en 8960  df-dom 8961  df-sdom 8962  df-fin 8963

This theorem is referenced by:  fin23lem23  10340