Theorem fin23lem26 10216

Description: Lemma for fin23lem22 10218. (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 5093	. . . 4 ⊢ (𝑖 = ∅ → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ ∅))
2	1	rexbidv 3156	. . 3 ⊢ (𝑖 = ∅ → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ ∅))
3		breq2 5093	. . . 4 ⊢ (𝑖 = 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ 𝑎))
4	3	rexbidv 3156	. . 3 ⊢ (𝑖 = 𝑎 → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎))
5		breq2 5093	. . . 4 ⊢ (𝑖 = suc 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ suc 𝑎))
6	5	rexbidv 3156	. . 3 ⊢ (𝑖 = suc 𝑎 → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎))
7		ordom 7806	. . . . 5 ⊢ Ord ω
8		simpl 482	. . . . 5 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ⊆ ω)
9		0fi 8964	. . . . . . . 8 ⊢ ∅ ∈ Fin
10		eleq1 2819	. . . . . . . 8 ⊢ (𝑆 = ∅ → (𝑆 ∈ Fin ↔ ∅ ∈ Fin))
11	9, 10	mpbiri 258	. . . . . . 7 ⊢ (𝑆 = ∅ → 𝑆 ∈ Fin)
12	11	necon3bi 2954	. . . . . 6 ⊢ (¬ 𝑆 ∈ Fin → 𝑆 ≠ ∅)
13	12	adantl 481	. . . . 5 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ≠ ∅)
14		tz7.5 6327	. . . . 5 ⊢ ((Ord ω ∧ 𝑆 ⊆ ω ∧ 𝑆 ≠ ∅) → ∃𝑗 ∈ 𝑆 (𝑆 ∩ 𝑗) = ∅)
15	7, 8, 13, 14	mp3an2i 1468	. . . 4 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗 ∈ 𝑆 (𝑆 ∩ 𝑗) = ∅)
16		en0 8940	. . . . . 6 ⊢ ((𝑗 ∩ 𝑆) ≈ ∅ ↔ (𝑗 ∩ 𝑆) = ∅)
17		incom 4156	. . . . . . 7 ⊢ (𝑗 ∩ 𝑆) = (𝑆 ∩ 𝑗)
18	17	eqeq1i 2736	. . . . . 6 ⊢ ((𝑗 ∩ 𝑆) = ∅ ↔ (𝑆 ∩ 𝑗) = ∅)
19	16, 18	bitri 275	. . . . 5 ⊢ ((𝑗 ∩ 𝑆) ≈ ∅ ↔ (𝑆 ∩ 𝑗) = ∅)
20	19	rexbii 3079	. . . 4 ⊢ (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ ∅ ↔ ∃𝑗 ∈ 𝑆 (𝑆 ∩ 𝑗) = ∅)
21	15, 20	sylibr 234	. . 3 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ ∅)
22		simplrl 776	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑆 ⊆ ω)
23		omsson 7800	. . . . . . . . . . 11 ⊢ ω ⊆ On
24	22, 23	sstrdi 3942	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑆 ⊆ On)
25	24	ssdifssd 4094	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ⊆ On)
26		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → ¬ 𝑆 ∈ Fin)
27		ssel2 3924	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ ω ∧ 𝑗 ∈ 𝑆) → 𝑗 ∈ ω)
28		onfin2 9125	. . . . . . . . . . . . . . . . 17 ⊢ ω = (On ∩ Fin)
29		inss2 4185	. . . . . . . . . . . . . . . . 17 ⊢ (On ∩ Fin) ⊆ Fin
30	28, 29	eqsstri 3976	. . . . . . . . . . . . . . . 16 ⊢ ω ⊆ Fin
31		peano2 7820	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ω → suc 𝑗 ∈ ω)
32	30, 31	sselid 3927	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ω → suc 𝑗 ∈ Fin)
33	27, 32	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ⊆ ω ∧ 𝑗 ∈ 𝑆) → suc 𝑗 ∈ Fin)
34	33	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → suc 𝑗 ∈ Fin)
35		ssfi 9082	. . . . . . . . . . . . . 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 4313	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) = ∅)
40	39	necon3bbii 2975	. . . . . . . . . . 11 ⊢ (¬ 𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) ≠ ∅)
41	38, 40	sylib 218	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → (𝑆 ∖ suc 𝑗) ≠ ∅)
42	41	ad2ant2lr 748	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ≠ ∅)
43		onint 7723	. . . . . . . . 9 ⊢ (((𝑆 ∖ suc 𝑗) ⊆ On ∧ (𝑆 ∖ suc 𝑗) ≠ ∅) → ∩ (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
44	25, 42, 43	syl2anc 584	. . . . . . . 8 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∩ (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
45	44	eldifad 3909	. . . . . . 7 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∩ (𝑆 ∖ suc 𝑗) ∈ 𝑆)
46		simprr 772	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑗 ∩ 𝑆) ≈ 𝑎)
47		en2sn 8963	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ V ∧ 𝑎 ∈ V) → {𝑗} ≈ {𝑎})
48	47	el2v 3443	. . . . . . . . . 10 ⊢ {𝑗} ≈ {𝑎}
49	48	a1i 11	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → {𝑗} ≈ {𝑎})
50		simprl 770	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑗 ∈ 𝑆)
51	22, 50	sseldd 3930	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑗 ∈ ω)
52		nnord 7804	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ω → Ord 𝑗)
53	51, 52	syl 17	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → Ord 𝑗)
54		ordirr 6324	. . . . . . . . . . . 12 ⊢ (Ord 𝑗 → ¬ 𝑗 ∈ 𝑗)
55		elinel1 4148	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (𝑗 ∩ 𝑆) → 𝑗 ∈ 𝑗)
56	54, 55	nsyl 140	. . . . . . . . . . 11 ⊢ (Ord 𝑗 → ¬ 𝑗 ∈ (𝑗 ∩ 𝑆))
57		disjsn 4661	. . . . . . . . . . 11 ⊢ (((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅ ↔ ¬ 𝑗 ∈ (𝑗 ∩ 𝑆))
58	56, 57	sylibr 234	. . . . . . . . . 10 ⊢ (Ord 𝑗 → ((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅)
59	53, 58	syl 17	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅)
60		nnord 7804	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ω → Ord 𝑎)
61		ordirr 6324	. . . . . . . . . . . 12 ⊢ (Ord 𝑎 → ¬ 𝑎 ∈ 𝑎)
62	60, 61	syl 17	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ω → ¬ 𝑎 ∈ 𝑎)
63		disjsn 4661	. . . . . . . . . . 11 ⊢ ((𝑎 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ 𝑎)
64	62, 63	sylibr 234	. . . . . . . . . 10 ⊢ (𝑎 ∈ ω → (𝑎 ∩ {𝑎}) = ∅)
65	64	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑎 ∩ {𝑎}) = ∅)
66		unen 8967	. . . . . . . . 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 3942	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → 𝑆 ⊆ On)
71		ordsuc 7744	. . . . . . . . . . . . . . . . . 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 4094	. . . . . . . . . . . . . . . . . . . 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 3908	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ (𝑆 ∖ suc 𝑗))
79	78	ex 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗 → 𝑏 ∈ (𝑆 ∖ suc 𝑗)))
80		onnmin 7731	. . . . . . . . . . . . . . . . . . . 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 7748	. . . . . . . . . . . . . . . . . . . . . 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 4093	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏))
89		intss 4917	. . . . . . . . . . . . . . . . . . 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 6330	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Ord suc 𝑗 ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
93	84, 92	sylan 580	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
94		onmindif 6400	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ⊆ On ∧ 𝑏 ∈ On) → 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑏))
95	91, 93, 94	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑏))
96	90, 95	sseldd 3930	. . . . . . . . . . . . . . . . 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 6312	. . . . . . . . . . . . . . . 16 ⊢ suc 𝑗 = (𝑗 ∪ {𝑗})
100	99	eleq2i 2823	. . . . . . . . . . . . . . 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 3913	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ∧ 𝑏 ∈ 𝑆))
105		elin 3913	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏 ∈ 𝑆))
106	103, 104, 105	3bitr4g 314	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑏 ∈ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ 𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆)))
107	106	eqrdv 2729	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∪ {𝑗}) ∩ 𝑆))
108		indir 4233	. . . . . . . . . 10 ⊢ ((𝑗 ∪ {𝑗}) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆))
109	107, 108	eqtrdi 2782	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)))
110		snssi 4757	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ 𝑆 → {𝑗} ⊆ 𝑆)
111		dfss2 3915	. . . . . . . . . . . 12 ⊢ ({𝑗} ⊆ 𝑆 ↔ ({𝑗} ∩ 𝑆) = {𝑗})
112	110, 111	sylib 218	. . . . . . . . . . 11 ⊢ (𝑗 ∈ 𝑆 → ({𝑗} ∩ 𝑆) = {𝑗})
113	112	uneq2d 4115	. . . . . . . . . 10 ⊢ (𝑗 ∈ 𝑆 → ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗 ∩ 𝑆) ∪ {𝑗}))
114	113	ad2antrl 728	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗 ∩ 𝑆) ∪ {𝑗}))
115	109, 114	eqtrd 2766	. . . . . . . 8 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ {𝑗}))
116		df-suc 6312	. . . . . . . . 9 ⊢ suc 𝑎 = (𝑎 ∪ {𝑎})
117	116	a1i 11	. . . . . . . 8 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → suc 𝑎 = (𝑎 ∪ {𝑎}))
118	67, 115, 117	3brtr4d 5121	. . . . . . 7 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎)
119		ineq1 4160	. . . . . . . . 9 ⊢ (𝑏 = ∩ (𝑆 ∖ suc 𝑗) → (𝑏 ∩ 𝑆) = (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆))
120	119	breq1d 5099	. . . . . . . 8 ⊢ (𝑏 = ∩ (𝑆 ∖ suc 𝑗) → ((𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎))
121	120	rspcev 3572	. . . . . . 7 ⊢ ((∩ (𝑆 ∖ suc 𝑗) ∈ 𝑆 ∧ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎) → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎)
122	45, 118, 121	syl2anc 584	. . . . . 6 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎)
123	122	rexlimdvaa 3134	. . . . 5 ⊢ ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎))
124		ineq1 4160	. . . . . . 7 ⊢ (𝑏 = 𝑗 → (𝑏 ∩ 𝑆) = (𝑗 ∩ 𝑆))
125	124	breq1d 5099	. . . . . 6 ⊢ (𝑏 = 𝑗 → ((𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ (𝑗 ∩ 𝑆) ≈ suc 𝑎))
126	125	cbvrexvw 3211	. . . . 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 7828	. 2 ⊢ (𝑖 ∈ ω → ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖))
130	129	impcom 407	1 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111   ≠ wne 2928  ∃wrex 3056  Vcvv 3436   ∖ cdif 3894   ∪ cun 3895   ∩ cin 3896   ⊆ wss 3897  ∅c0 4280  {csn 4573  ∩ cint 4895   class class class wbr 5089  Ord word 6305  Oncon0 6306  suc csuc 6308  ωcom 7796   ≈ cen 8866  Fincfn 8869

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-int 4896  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-om 7797  df-1o 8385  df-en 8870  df-dom 8871  df-sdom 8872  df-fin 8873

This theorem is referenced by:  fin23lem23  10217