Theorem fin23lem26 9736

Description: Lemma for fin23lem22 9738. (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 5034	. . . 4 ⊢ (𝑖 = ∅ → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ ∅))
2	1	rexbidv 3256	. . 3 ⊢ (𝑖 = ∅ → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ ∅))
3		breq2 5034	. . . 4 ⊢ (𝑖 = 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ 𝑎))
4	3	rexbidv 3256	. . 3 ⊢ (𝑖 = 𝑎 → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎))
5		breq2 5034	. . . 4 ⊢ (𝑖 = suc 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ suc 𝑎))
6	5	rexbidv 3256	. . 3 ⊢ (𝑖 = suc 𝑎 → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎))
7		ordom 7569	. . . . 5 ⊢ Ord ω
8		simpl 486	. . . . 5 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ⊆ ω)
9		0fin 8730	. . . . . . . 8 ⊢ ∅ ∈ Fin
10		eleq1 2877	. . . . . . . 8 ⊢ (𝑆 = ∅ → (𝑆 ∈ Fin ↔ ∅ ∈ Fin))
11	9, 10	mpbiri 261	. . . . . . 7 ⊢ (𝑆 = ∅ → 𝑆 ∈ Fin)
12	11	necon3bi 3013	. . . . . 6 ⊢ (¬ 𝑆 ∈ Fin → 𝑆 ≠ ∅)
13	12	adantl 485	. . . . 5 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ≠ ∅)
14		tz7.5 6180	. . . . 5 ⊢ ((Ord ω ∧ 𝑆 ⊆ ω ∧ 𝑆 ≠ ∅) → ∃𝑗 ∈ 𝑆 (𝑆 ∩ 𝑗) = ∅)
15	7, 8, 13, 14	mp3an2i 1463	. . . 4 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗 ∈ 𝑆 (𝑆 ∩ 𝑗) = ∅)
16		en0 8555	. . . . . 6 ⊢ ((𝑗 ∩ 𝑆) ≈ ∅ ↔ (𝑗 ∩ 𝑆) = ∅)
17		incom 4128	. . . . . . 7 ⊢ (𝑗 ∩ 𝑆) = (𝑆 ∩ 𝑗)
18	17	eqeq1i 2803	. . . . . 6 ⊢ ((𝑗 ∩ 𝑆) = ∅ ↔ (𝑆 ∩ 𝑗) = ∅)
19	16, 18	bitri 278	. . . . 5 ⊢ ((𝑗 ∩ 𝑆) ≈ ∅ ↔ (𝑆 ∩ 𝑗) = ∅)
20	19	rexbii 3210	. . . 4 ⊢ (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ ∅ ↔ ∃𝑗 ∈ 𝑆 (𝑆 ∩ 𝑗) = ∅)
21	15, 20	sylibr 237	. . 3 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ ∅)
22		simplrl 776	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑆 ⊆ ω)
23		omsson 7564	. . . . . . . . . . 11 ⊢ ω ⊆ On
24	22, 23	sstrdi 3927	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑆 ⊆ On)
25	24	ssdifssd 4070	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ⊆ On)
26		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → ¬ 𝑆 ∈ Fin)
27		ssel2 3910	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ ω ∧ 𝑗 ∈ 𝑆) → 𝑗 ∈ ω)
28		onfin2 8695	. . . . . . . . . . . . . . . . 17 ⊢ ω = (On ∩ Fin)
29		inss2 4156	. . . . . . . . . . . . . . . . 17 ⊢ (On ∩ Fin) ⊆ Fin
30	28, 29	eqsstri 3949	. . . . . . . . . . . . . . . 16 ⊢ ω ⊆ Fin
31		peano2 7582	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ω → suc 𝑗 ∈ ω)
32	30, 31	sseldi 3913	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ω → suc 𝑗 ∈ Fin)
33	27, 32	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ⊆ ω ∧ 𝑗 ∈ 𝑆) → suc 𝑗 ∈ Fin)
34	33	adantlr 714	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → suc 𝑗 ∈ Fin)
35		ssfi 8722	. . . . . . . . . . . . . 14 ⊢ ((suc 𝑗 ∈ Fin ∧ 𝑆 ⊆ suc 𝑗) → 𝑆 ∈ Fin)
36	35	ex 416	. . . . . . . . . . . . 13 ⊢ (suc 𝑗 ∈ Fin → (𝑆 ⊆ suc 𝑗 → 𝑆 ∈ Fin))
37	34, 36	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → (𝑆 ⊆ suc 𝑗 → 𝑆 ∈ Fin))
38	26, 37	mtod 201	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → ¬ 𝑆 ⊆ suc 𝑗)
39		ssdif0 4277	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) = ∅)
40	39	necon3bbii 3034	. . . . . . . . . . 11 ⊢ (¬ 𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) ≠ ∅)
41	38, 40	sylib 221	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → (𝑆 ∖ suc 𝑗) ≠ ∅)
42	41	ad2ant2lr 747	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ≠ ∅)
43		onint 7490	. . . . . . . . 9 ⊢ (((𝑆 ∖ suc 𝑗) ⊆ On ∧ (𝑆 ∖ suc 𝑗) ≠ ∅) → ∩ (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
44	25, 42, 43	syl2anc 587	. . . . . . . 8 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∩ (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
45	44	eldifad 3893	. . . . . . 7 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∩ (𝑆 ∖ suc 𝑗) ∈ 𝑆)
46		simprr 772	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑗 ∩ 𝑆) ≈ 𝑎)
47		en2sn 8576	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ V ∧ 𝑎 ∈ V) → {𝑗} ≈ {𝑎})
48	47	el2v 3448	. . . . . . . . . 10 ⊢ {𝑗} ≈ {𝑎}
49	48	a1i 11	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → {𝑗} ≈ {𝑎})
50		simprl 770	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑗 ∈ 𝑆)
51	22, 50	sseldd 3916	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑗 ∈ ω)
52		nnord 7568	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ω → Ord 𝑗)
53	51, 52	syl 17	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → Ord 𝑗)
54		ordirr 6177	. . . . . . . . . . . 12 ⊢ (Ord 𝑗 → ¬ 𝑗 ∈ 𝑗)
55		elinel1 4122	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (𝑗 ∩ 𝑆) → 𝑗 ∈ 𝑗)
56	54, 55	nsyl 142	. . . . . . . . . . 11 ⊢ (Ord 𝑗 → ¬ 𝑗 ∈ (𝑗 ∩ 𝑆))
57		disjsn 4607	. . . . . . . . . . 11 ⊢ (((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅ ↔ ¬ 𝑗 ∈ (𝑗 ∩ 𝑆))
58	56, 57	sylibr 237	. . . . . . . . . 10 ⊢ (Ord 𝑗 → ((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅)
59	53, 58	syl 17	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅)
60		nnord 7568	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ω → Ord 𝑎)
61		ordirr 6177	. . . . . . . . . . . 12 ⊢ (Ord 𝑎 → ¬ 𝑎 ∈ 𝑎)
62	60, 61	syl 17	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ω → ¬ 𝑎 ∈ 𝑎)
63		disjsn 4607	. . . . . . . . . . 11 ⊢ ((𝑎 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ 𝑎)
64	62, 63	sylibr 237	. . . . . . . . . 10 ⊢ (𝑎 ∈ ω → (𝑎 ∩ {𝑎}) = ∅)
65	64	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑎 ∩ {𝑎}) = ∅)
66		unen 8579	. . . . . . . . 9 ⊢ ((((𝑗 ∩ 𝑆) ≈ 𝑎 ∧ {𝑗} ≈ {𝑎}) ∧ (((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅ ∧ (𝑎 ∩ {𝑎}) = ∅)) → ((𝑗 ∩ 𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎}))
67	46, 49, 59, 65, 66	syl22anc 837	. . . . . . . 8 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎}))
68		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → 𝑏 ∈ 𝑆)
69		simplrl 776	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → 𝑆 ⊆ ω)
70	69, 23	sstrdi 3927	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → 𝑆 ⊆ On)
71		ordsuc 7509	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord 𝑗 ↔ Ord suc 𝑗)
72	53, 71	sylib 221	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → Ord suc 𝑗)
73	72	adantrr 716	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → Ord suc 𝑗)
74		simp2 1134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → 𝑆 ⊆ On)
75	74	ssdifssd 4070	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ On)
76		simpl1 1188	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ 𝑆)
77		simpr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → ¬ 𝑏 ∈ suc 𝑗)
78	76, 77	eldifd 3892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ (𝑆 ∖ suc 𝑗))
79	78	ex 416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗 → 𝑏 ∈ (𝑆 ∖ suc 𝑗)))
80		onnmin 7498	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ∖ suc 𝑗) ⊆ On ∧ 𝑏 ∈ (𝑆 ∖ suc 𝑗)) → ¬ 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗))
81	75, 79, 80	syl6an 683	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗 → ¬ 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗)))
82	81	con4d 115	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) → 𝑏 ∈ suc 𝑗))
83	82	imp 410	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗)) → 𝑏 ∈ suc 𝑗)
84		simp3 1135	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → Ord suc 𝑗)
85		ordsucss 7513	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Ord suc 𝑗 → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗))
86	84, 85	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗))
87	86	imp 410	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → suc 𝑏 ⊆ suc 𝑗)
88	87	sscond 4069	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏))
89		intss 4859	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏) → ∩ (𝑆 ∖ suc 𝑏) ⊆ ∩ (𝑆 ∖ suc 𝑗))
90	88, 89	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → ∩ (𝑆 ∖ suc 𝑏) ⊆ ∩ (𝑆 ∖ suc 𝑗))
91		simpl2 1189	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑆 ⊆ On)
92		ordelon 6183	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Ord suc 𝑗 ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
93	84, 92	sylan 583	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
94		onmindif 6248	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ⊆ On ∧ 𝑏 ∈ On) → 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑏))
95	91, 93, 94	syl2anc 587	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑏))
96	90, 95	sseldd 3916	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗))
97	83, 96	impbida 800	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗))
98	68, 70, 73, 97	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗))
99		df-suc 6165	. . . . . . . . . . . . . . . 16 ⊢ suc 𝑗 = (𝑗 ∪ {𝑗})
100	99	eleq2i 2881	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ suc 𝑗 ↔ 𝑏 ∈ (𝑗 ∪ {𝑗}))
101	98, 100	syl6bb 290	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗})))
102	101	expr 460	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑏 ∈ 𝑆 → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗}))))
103	102	pm5.32rd 581	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ∧ 𝑏 ∈ 𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏 ∈ 𝑆)))
104		elin 3897	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ∧ 𝑏 ∈ 𝑆))
105		elin 3897	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏 ∈ 𝑆))
106	103, 104, 105	3bitr4g 317	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑏 ∈ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ 𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆)))
107	106	eqrdv 2796	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∪ {𝑗}) ∩ 𝑆))
108		indir 4202	. . . . . . . . . 10 ⊢ ((𝑗 ∪ {𝑗}) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆))
109	107, 108	eqtrdi 2849	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)))
110		snssi 4701	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ 𝑆 → {𝑗} ⊆ 𝑆)
111		df-ss 3898	. . . . . . . . . . . 12 ⊢ ({𝑗} ⊆ 𝑆 ↔ ({𝑗} ∩ 𝑆) = {𝑗})
112	110, 111	sylib 221	. . . . . . . . . . 11 ⊢ (𝑗 ∈ 𝑆 → ({𝑗} ∩ 𝑆) = {𝑗})
113	112	uneq2d 4090	. . . . . . . . . 10 ⊢ (𝑗 ∈ 𝑆 → ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗 ∩ 𝑆) ∪ {𝑗}))
114	113	ad2antrl 727	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗 ∩ 𝑆) ∪ {𝑗}))
115	109, 114	eqtrd 2833	. . . . . . . 8 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ {𝑗}))
116		df-suc 6165	. . . . . . . . 9 ⊢ suc 𝑎 = (𝑎 ∪ {𝑎})
117	116	a1i 11	. . . . . . . 8 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → suc 𝑎 = (𝑎 ∪ {𝑎}))
118	67, 115, 117	3brtr4d 5062	. . . . . . 7 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎)
119		ineq1 4131	. . . . . . . . 9 ⊢ (𝑏 = ∩ (𝑆 ∖ suc 𝑗) → (𝑏 ∩ 𝑆) = (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆))
120	119	breq1d 5040	. . . . . . . 8 ⊢ (𝑏 = ∩ (𝑆 ∖ suc 𝑗) → ((𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎))
121	120	rspcev 3571	. . . . . . 7 ⊢ ((∩ (𝑆 ∖ suc 𝑗) ∈ 𝑆 ∧ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎) → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎)
122	45, 118, 121	syl2anc 587	. . . . . 6 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎)
123	122	rexlimdvaa 3244	. . . . 5 ⊢ ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎))
124		ineq1 4131	. . . . . . 7 ⊢ (𝑏 = 𝑗 → (𝑏 ∩ 𝑆) = (𝑗 ∩ 𝑆))
125	124	breq1d 5040	. . . . . 6 ⊢ (𝑏 = 𝑗 → ((𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ (𝑗 ∩ 𝑆) ≈ suc 𝑎))
126	125	cbvrexvw 3397	. . . . 5 ⊢ (∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎)
127	123, 126	syl6ib 254	. . . 4 ⊢ ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎))
128	127	ex 416	. . 3 ⊢ (𝑎 ∈ ω → ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎)))
129	2, 4, 6, 21, 128	finds2 7591	. 2 ⊢ (𝑖 ∈ ω → ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖))
130	129	impcom 411	1 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∃wrex 3107  Vcvv 3441   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  {csn 4525  ∩ cint 4838   class class class wbr 5030  Ord word 6158  Oncon0 6159  suc csuc 6161  ωcom 7560   ≈ cen 8489  Fincfn 8492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-br 5031  df-opab 5093  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-om 7561  df-1o 8085  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496

This theorem is referenced by:  fin23lem23  9737