Theorem fin23lem26 10330

Description: Lemma for fin23lem22 10332. (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 5111	. . . 4 ⊢ (𝑖 = ∅ → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ ∅))
2	1	rexbidv 3188	. . 3 ⊢ (𝑖 = ∅ → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ ∅))
3		breq2 5111	. . . 4 ⊢ (𝑖 = 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ 𝑎))
4	3	rexbidv 3188	. . 3 ⊢ (𝑖 = 𝑎 → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎))
5		breq2 5111	. . . 4 ⊢ (𝑖 = suc 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ suc 𝑎))
6	5	rexbidv 3188	. . 3 ⊢ (𝑖 = suc 𝑎 → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎))
7		ordom 7875	. . . . 5 ⊢ Ord ω
8		simpl 488	. . . . 5 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ⊆ ω)
9		0fi 9052	. . . . . . . 8 ⊢ ∅ ∈ Fin
10		eleq1 2850	. . . . . . . 8 ⊢ (𝑆 = ∅ → (𝑆 ∈ Fin ↔ ∅ ∈ Fin))
11	9, 10	mpbiri 261	. . . . . . 7 ⊢ (𝑆 = ∅ → 𝑆 ∈ Fin)
12	11	necon3bi 2983	. . . . . 6 ⊢ (¬ 𝑆 ∈ Fin → 𝑆 ≠ ∅)
13	12	adantl 487	. . . . 5 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ≠ ∅)
14		tz7.5 6382	. . . . 5 ⊢ ((Ord ω ∧ 𝑆 ⊆ ω ∧ 𝑆 ≠ ∅) → ∃𝑗 ∈ 𝑆 (𝑆 ∩ 𝑗) = ∅)
15	7, 8, 13, 14	mp3an2i 1495	. . . 4 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗 ∈ 𝑆 (𝑆 ∩ 𝑗) = ∅)
16		en0 9027	. . . . . 6 ⊢ ((𝑗 ∩ 𝑆) ≈ ∅ ↔ (𝑗 ∩ 𝑆) = ∅)
17		incom 4158	. . . . . . 7 ⊢ (𝑗 ∩ 𝑆) = (𝑆 ∩ 𝑗)
18	17	eqeq1i 2767	. . . . . 6 ⊢ ((𝑗 ∩ 𝑆) = ∅ ↔ (𝑆 ∩ 𝑗) = ∅)
19	16, 18	bitri 278	. . . . 5 ⊢ ((𝑗 ∩ 𝑆) ≈ ∅ ↔ (𝑆 ∩ 𝑗) = ∅)
20	19	rexbii 3111	. . . 4 ⊢ (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ ∅ ↔ ∃𝑗 ∈ 𝑆 (𝑆 ∩ 𝑗) = ∅)
21	15, 20	sylibr 237	. . 3 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ ∅)
22		simplrl 789	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑆 ⊆ ω)
23		omsson 7869	. . . . . . . . . . 11 ⊢ ω ⊆ On
24	22, 23	sstrdi 3946	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑆 ⊆ On)
25	24	ssdifssd 4097	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ⊆ On)
26		simplr 781	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → ¬ 𝑆 ∈ Fin)
27		ssel2 3929	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ ω ∧ 𝑗 ∈ 𝑆) → 𝑗 ∈ ω)
28		onfin2 9214	. . . . . . . . . . . . . . . . 17 ⊢ ω = (On ∩ Fin)
29		inss2 4186	. . . . . . . . . . . . . . . . 17 ⊢ (On ∩ Fin) ⊆ Fin
30	28, 29	eqsstri 3980	. . . . . . . . . . . . . . . 16 ⊢ ω ⊆ Fin
31		peano2 7889	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ω → suc 𝑗 ∈ ω)
32	30, 31	sselid 3932	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ω → suc 𝑗 ∈ Fin)
33	27, 32	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ⊆ ω ∧ 𝑗 ∈ 𝑆) → suc 𝑗 ∈ Fin)
34	33	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → suc 𝑗 ∈ Fin)
35		ssfi 9170	. . . . . . . . . . . . . 14 ⊢ ((suc 𝑗 ∈ Fin ∧ 𝑆 ⊆ suc 𝑗) → 𝑆 ∈ Fin)
36	35	ex 418	. . . . . . . . . . . . 13 ⊢ (suc 𝑗 ∈ Fin → (𝑆 ⊆ suc 𝑗 → 𝑆 ∈ Fin))
37	34, 36	syl 18	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → (𝑆 ⊆ suc 𝑗 → 𝑆 ∈ Fin))
38	26, 37	mtod 201	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → ¬ 𝑆 ⊆ suc 𝑗)
39		ssdif0 4317	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) = ∅)
40	39	necon3bbii 3004	. . . . . . . . . . 11 ⊢ (¬ 𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) ≠ ∅)
41	38, 40	sylib 221	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → (𝑆 ∖ suc 𝑗) ≠ ∅)
42	41	ad2ant2lr 761	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ≠ ∅)
43		onint 7792	. . . . . . . . 9 ⊢ (((𝑆 ∖ suc 𝑗) ⊆ On ∧ (𝑆 ∖ suc 𝑗) ≠ ∅) → ∩ (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
44	25, 42, 43	syl2anc 596	. . . . . . . 8 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∩ (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
45	44	eldifad 3914	. . . . . . 7 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∩ (𝑆 ∖ suc 𝑗) ∈ 𝑆)
46		simprr 785	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑗 ∩ 𝑆) ≈ 𝑎)
47		en2sn 9051	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ V ∧ 𝑎 ∈ V) → {𝑗} ≈ {𝑎})
48	47	el2v 3460	. . . . . . . . . 10 ⊢ {𝑗} ≈ {𝑎}
49	48	a1i 11	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → {𝑗} ≈ {𝑎})
50		simprl 783	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑗 ∈ 𝑆)
51	22, 50	sseldd 3935	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑗 ∈ ω)
52		nnord 7873	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ω → Ord 𝑗)
53	51, 52	syl 18	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → Ord 𝑗)
54		ordirr 6379	. . . . . . . . . . . 12 ⊢ (Ord 𝑗 → ¬ 𝑗 ∈ 𝑗)
55		elinel1 4150	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (𝑗 ∩ 𝑆) → 𝑗 ∈ 𝑗)
56	54, 55	nsyl 141	. . . . . . . . . . 11 ⊢ (Ord 𝑗 → ¬ 𝑗 ∈ (𝑗 ∩ 𝑆))
57		disjsn 4675	. . . . . . . . . . 11 ⊢ (((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅ ↔ ¬ 𝑗 ∈ (𝑗 ∩ 𝑆))
58	56, 57	sylibr 237	. . . . . . . . . 10 ⊢ (Ord 𝑗 → ((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅)
59	53, 58	syl 18	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅)
60		nnord 7873	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ω → Ord 𝑎)
61		ordirr 6379	. . . . . . . . . . . 12 ⊢ (Ord 𝑎 → ¬ 𝑎 ∈ 𝑎)
62	60, 61	syl 18	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ω → ¬ 𝑎 ∈ 𝑎)
63		disjsn 4675	. . . . . . . . . . 11 ⊢ ((𝑎 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ 𝑎)
64	62, 63	sylibr 237	. . . . . . . . . 10 ⊢ (𝑎 ∈ ω → (𝑎 ∩ {𝑎}) = ∅)
65	64	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑎 ∩ {𝑎}) = ∅)
66		unen 9055	. . . . . . . . 9 ⊢ ((((𝑗 ∩ 𝑆) ≈ 𝑎 ∧ {𝑗} ≈ {𝑎}) ∧ (((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅ ∧ (𝑎 ∩ {𝑎}) = ∅)) → ((𝑗 ∩ 𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎}))
67	46, 49, 59, 65, 66	syl22anc 852	. . . . . . . 8 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎}))
68		simprr 785	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → 𝑏 ∈ 𝑆)
69		simplrl 789	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → 𝑆 ⊆ ω)
70	69, 23	sstrdi 3946	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → 𝑆 ⊆ On)
71		ordsuc 7813	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord 𝑗 ↔ Ord suc 𝑗)
72	53, 71	sylib 221	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → Ord suc 𝑗)
73	72	adantrr 730	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → Ord suc 𝑗)
74		simp2 1155	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → 𝑆 ⊆ On)
75	74	ssdifssd 4097	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ On)
76		simpl1 1210	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ 𝑆)
77		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → ¬ 𝑏 ∈ suc 𝑗)
78	76, 77	eldifd 3913	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ (𝑆 ∖ suc 𝑗))
79	78	ex 418	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗 → 𝑏 ∈ (𝑆 ∖ suc 𝑗)))
80		onnmin 7800	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ∖ suc 𝑗) ⊆ On ∧ 𝑏 ∈ (𝑆 ∖ suc 𝑗)) → ¬ 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗))
81	75, 79, 80	syl6an 697	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗 → ¬ 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗)))
82	81	con4d 116	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) → 𝑏 ∈ suc 𝑗))
83	82	imp 412	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗)) → 𝑏 ∈ suc 𝑗)
84		simp3 1156	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → Ord suc 𝑗)
85		ordsucss 7817	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Ord suc 𝑗 → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗))
86	84, 85	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗))
87	86	imp 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → suc 𝑏 ⊆ suc 𝑗)
88	87	sscond 4096	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏))
89		intss 4932	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏) → ∩ (𝑆 ∖ suc 𝑏) ⊆ ∩ (𝑆 ∖ suc 𝑗))
90	88, 89	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → ∩ (𝑆 ∖ suc 𝑏) ⊆ ∩ (𝑆 ∖ suc 𝑗))
91		simpl2 1211	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑆 ⊆ On)
92		ordelon 6385	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Ord suc 𝑗 ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
93	84, 92	sylan 592	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
94		onmindif 6456	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ⊆ On ∧ 𝑏 ∈ On) → 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑏))
95	91, 93, 94	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑏))
96	90, 95	sseldd 3935	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗))
97	83, 96	impbida 813	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗))
98	68, 70, 73, 97	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗))
99		df-suc 6367	. . . . . . . . . . . . . . . 16 ⊢ suc 𝑗 = (𝑗 ∪ {𝑗})
100	99	eleq2i 2854	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ suc 𝑗 ↔ 𝑏 ∈ (𝑗 ∪ {𝑗}))
101	98, 100	bitrdi 290	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗})))
102	101	expr 462	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑏 ∈ 𝑆 → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗}))))
103	102	pm5.32rd 589	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ∧ 𝑏 ∈ 𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏 ∈ 𝑆)))
104		elin 3918	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ∧ 𝑏 ∈ 𝑆))
105		elin 3918	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏 ∈ 𝑆))
106	103, 104, 105	3bitr4g 317	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑏 ∈ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ 𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆)))
107	106	eqrdv 2760	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∪ {𝑗}) ∩ 𝑆))
108		indir 4235	. . . . . . . . . 10 ⊢ ((𝑗 ∪ {𝑗}) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆))
109	107, 108	eqtrdi 2813	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)))
110		snssi 4749	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ 𝑆 → {𝑗} ⊆ 𝑆)
111		dfss2 3920	. . . . . . . . . . . 12 ⊢ ({𝑗} ⊆ 𝑆 ↔ ({𝑗} ∩ 𝑆) = {𝑗})
112	110, 111	sylib 221	. . . . . . . . . . 11 ⊢ (𝑗 ∈ 𝑆 → ({𝑗} ∩ 𝑆) = {𝑗})
113	112	uneq2d 4118	. . . . . . . . . 10 ⊢ (𝑗 ∈ 𝑆 → ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗 ∩ 𝑆) ∪ {𝑗}))
114	113	ad2antrl 741	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗 ∩ 𝑆) ∪ {𝑗}))
115	109, 114	eqtrd 2797	. . . . . . . 8 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ {𝑗}))
116		df-suc 6367	. . . . . . . . 9 ⊢ suc 𝑎 = (𝑎 ∪ {𝑎})
117	116	a1i 11	. . . . . . . 8 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → suc 𝑎 = (𝑎 ∪ {𝑎}))
118	67, 115, 117	3brtr4d 5141	. . . . . . 7 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎)
119		ineq1 4162	. . . . . . . . 9 ⊢ (𝑏 = ∩ (𝑆 ∖ suc 𝑗) → (𝑏 ∩ 𝑆) = (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆))
120	119	breq1d 5117	. . . . . . . 8 ⊢ (𝑏 = ∩ (𝑆 ∖ suc 𝑗) → ((𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎))
121	120	rspcev 3579	. . . . . . 7 ⊢ ((∩ (𝑆 ∖ suc 𝑗) ∈ 𝑆 ∧ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎) → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎)
122	45, 118, 121	syl2anc 596	. . . . . 6 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎)
123	122	rexlimdvaa 3166	. . . . 5 ⊢ ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎))
124		ineq1 4162	. . . . . . 7 ⊢ (𝑏 = 𝑗 → (𝑏 ∩ 𝑆) = (𝑗 ∩ 𝑆))
125	124	breq1d 5117	. . . . . 6 ⊢ (𝑏 = 𝑗 → ((𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ (𝑗 ∩ 𝑆) ≈ suc 𝑎))
126	125	cbvrexvw 3243	. . . . 5 ⊢ (∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎)
127	123, 126	imbitrdi 254	. . . 4 ⊢ ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎))
128	127	ex 418	. . 3 ⊢ (𝑎 ∈ ω → ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎)))
129	2, 4, 6, 21, 128	finds2 7898	. 2 ⊢ (𝑖 ∈ ω → ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖))
130	129	impcom 413	1 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2957  ∃wrex 3088  Vcvv 3453   ∖ cdif 3899   ∪ cun 3900   ∩ cin 3901   ⊆ wss 3902  ∅c0 4282  {csn 4587  ∩ cint 4910   class class class wbr 5107  Ord word 6360  Oncon0 6361  suc csuc 6363  ωcom 7865   ≈ cen 8952  Fincfn 8955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7739

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-int 4911  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-om 7866  df-1o 8458  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959

This theorem is used by:  fin23lem23  10331