Theorem fin23lem26 9749

Description: Lemma for fin23lem22 9751. (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 5072	. . . 4 ⊢ (𝑖 = ∅ → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ ∅))
2	1	rexbidv 3299	. . 3 ⊢ (𝑖 = ∅ → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ ∅))
3		breq2 5072	. . . 4 ⊢ (𝑖 = 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ 𝑎))
4	3	rexbidv 3299	. . 3 ⊢ (𝑖 = 𝑎 → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎))
5		breq2 5072	. . . 4 ⊢ (𝑖 = suc 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ suc 𝑎))
6	5	rexbidv 3299	. . 3 ⊢ (𝑖 = suc 𝑎 → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎))
7		ordom 7591	. . . . 5 ⊢ Ord ω
8		simpl 485	. . . . 5 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ⊆ ω)
9		0fin 8748	. . . . . . . 8 ⊢ ∅ ∈ Fin
10		eleq1 2902	. . . . . . . 8 ⊢ (𝑆 = ∅ → (𝑆 ∈ Fin ↔ ∅ ∈ Fin))
11	9, 10	mpbiri 260	. . . . . . 7 ⊢ (𝑆 = ∅ → 𝑆 ∈ Fin)
12	11	necon3bi 3044	. . . . . 6 ⊢ (¬ 𝑆 ∈ Fin → 𝑆 ≠ ∅)
13	12	adantl 484	. . . . 5 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ≠ ∅)
14		tz7.5 6214	. . . . 5 ⊢ ((Ord ω ∧ 𝑆 ⊆ ω ∧ 𝑆 ≠ ∅) → ∃𝑗 ∈ 𝑆 (𝑆 ∩ 𝑗) = ∅)
15	7, 8, 13, 14	mp3an2i 1462	. . . 4 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗 ∈ 𝑆 (𝑆 ∩ 𝑗) = ∅)
16		en0 8574	. . . . . 6 ⊢ ((𝑗 ∩ 𝑆) ≈ ∅ ↔ (𝑗 ∩ 𝑆) = ∅)
17		incom 4180	. . . . . . 7 ⊢ (𝑗 ∩ 𝑆) = (𝑆 ∩ 𝑗)
18	17	eqeq1i 2828	. . . . . 6 ⊢ ((𝑗 ∩ 𝑆) = ∅ ↔ (𝑆 ∩ 𝑗) = ∅)
19	16, 18	bitri 277	. . . . 5 ⊢ ((𝑗 ∩ 𝑆) ≈ ∅ ↔ (𝑆 ∩ 𝑗) = ∅)
20	19	rexbii 3249	. . . 4 ⊢ (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ ∅ ↔ ∃𝑗 ∈ 𝑆 (𝑆 ∩ 𝑗) = ∅)
21	15, 20	sylibr 236	. . 3 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ ∅)
22		simplrl 775	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑆 ⊆ ω)
23		omsson 7586	. . . . . . . . . . 11 ⊢ ω ⊆ On
24	22, 23	sstrdi 3981	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑆 ⊆ On)
25	24	ssdifssd 4121	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ⊆ On)
26		simplr 767	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → ¬ 𝑆 ∈ Fin)
27		ssel2 3964	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ ω ∧ 𝑗 ∈ 𝑆) → 𝑗 ∈ ω)
28		onfin2 8712	. . . . . . . . . . . . . . . . 17 ⊢ ω = (On ∩ Fin)
29		inss2 4208	. . . . . . . . . . . . . . . . 17 ⊢ (On ∩ Fin) ⊆ Fin
30	28, 29	eqsstri 4003	. . . . . . . . . . . . . . . 16 ⊢ ω ⊆ Fin
31		peano2 7604	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ω → suc 𝑗 ∈ ω)
32	30, 31	sseldi 3967	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ω → suc 𝑗 ∈ Fin)
33	27, 32	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ⊆ ω ∧ 𝑗 ∈ 𝑆) → suc 𝑗 ∈ Fin)
34	33	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → suc 𝑗 ∈ Fin)
35		ssfi 8740	. . . . . . . . . . . . . 14 ⊢ ((suc 𝑗 ∈ Fin ∧ 𝑆 ⊆ suc 𝑗) → 𝑆 ∈ Fin)
36	35	ex 415	. . . . . . . . . . . . 13 ⊢ (suc 𝑗 ∈ Fin → (𝑆 ⊆ suc 𝑗 → 𝑆 ∈ Fin))
37	34, 36	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → (𝑆 ⊆ suc 𝑗 → 𝑆 ∈ Fin))
38	26, 37	mtod 200	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → ¬ 𝑆 ⊆ suc 𝑗)
39		ssdif0 4325	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) = ∅)
40	39	necon3bbii 3065	. . . . . . . . . . 11 ⊢ (¬ 𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) ≠ ∅)
41	38, 40	sylib 220	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → (𝑆 ∖ suc 𝑗) ≠ ∅)
42	41	ad2ant2lr 746	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ≠ ∅)
43		onint 7512	. . . . . . . . 9 ⊢ (((𝑆 ∖ suc 𝑗) ⊆ On ∧ (𝑆 ∖ suc 𝑗) ≠ ∅) → ∩ (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
44	25, 42, 43	syl2anc 586	. . . . . . . 8 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∩ (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
45	44	eldifad 3950	. . . . . . 7 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∩ (𝑆 ∖ suc 𝑗) ∈ 𝑆)
46		simprr 771	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑗 ∩ 𝑆) ≈ 𝑎)
47		en2sn 8595	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ V ∧ 𝑎 ∈ V) → {𝑗} ≈ {𝑎})
48	47	el2v 3503	. . . . . . . . . 10 ⊢ {𝑗} ≈ {𝑎}
49	48	a1i 11	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → {𝑗} ≈ {𝑎})
50		simprl 769	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑗 ∈ 𝑆)
51	22, 50	sseldd 3970	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑗 ∈ ω)
52		nnord 7590	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ω → Ord 𝑗)
53	51, 52	syl 17	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → Ord 𝑗)
54		ordirr 6211	. . . . . . . . . . . 12 ⊢ (Ord 𝑗 → ¬ 𝑗 ∈ 𝑗)
55		elinel1 4174	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (𝑗 ∩ 𝑆) → 𝑗 ∈ 𝑗)
56	54, 55	nsyl 142	. . . . . . . . . . 11 ⊢ (Ord 𝑗 → ¬ 𝑗 ∈ (𝑗 ∩ 𝑆))
57		disjsn 4649	. . . . . . . . . . 11 ⊢ (((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅ ↔ ¬ 𝑗 ∈ (𝑗 ∩ 𝑆))
58	56, 57	sylibr 236	. . . . . . . . . 10 ⊢ (Ord 𝑗 → ((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅)
59	53, 58	syl 17	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅)
60		nnord 7590	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ω → Ord 𝑎)
61		ordirr 6211	. . . . . . . . . . . 12 ⊢ (Ord 𝑎 → ¬ 𝑎 ∈ 𝑎)
62	60, 61	syl 17	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ω → ¬ 𝑎 ∈ 𝑎)
63		disjsn 4649	. . . . . . . . . . 11 ⊢ ((𝑎 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ 𝑎)
64	62, 63	sylibr 236	. . . . . . . . . 10 ⊢ (𝑎 ∈ ω → (𝑎 ∩ {𝑎}) = ∅)
65	64	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑎 ∩ {𝑎}) = ∅)
66		unen 8598	. . . . . . . . 9 ⊢ ((((𝑗 ∩ 𝑆) ≈ 𝑎 ∧ {𝑗} ≈ {𝑎}) ∧ (((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅ ∧ (𝑎 ∩ {𝑎}) = ∅)) → ((𝑗 ∩ 𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎}))
67	46, 49, 59, 65, 66	syl22anc 836	. . . . . . . 8 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎}))
68		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → 𝑏 ∈ 𝑆)
69		simplrl 775	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → 𝑆 ⊆ ω)
70	69, 23	sstrdi 3981	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → 𝑆 ⊆ On)
71		ordsuc 7531	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord 𝑗 ↔ Ord suc 𝑗)
72	53, 71	sylib 220	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → Ord suc 𝑗)
73	72	adantrr 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → Ord suc 𝑗)
74		simp2 1133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → 𝑆 ⊆ On)
75	74	ssdifssd 4121	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ On)
76		simpl1 1187	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ 𝑆)
77		simpr 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → ¬ 𝑏 ∈ suc 𝑗)
78	76, 77	eldifd 3949	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ (𝑆 ∖ suc 𝑗))
79	78	ex 415	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗 → 𝑏 ∈ (𝑆 ∖ suc 𝑗)))
80		onnmin 7520	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ∖ suc 𝑗) ⊆ On ∧ 𝑏 ∈ (𝑆 ∖ suc 𝑗)) → ¬ 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗))
81	75, 79, 80	syl6an 682	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗 → ¬ 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗)))
82	81	con4d 115	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) → 𝑏 ∈ suc 𝑗))
83	82	imp 409	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗)) → 𝑏 ∈ suc 𝑗)
84		simp3 1134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → Ord suc 𝑗)
85		ordsucss 7535	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Ord suc 𝑗 → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗))
86	84, 85	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗))
87	86	imp 409	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → suc 𝑏 ⊆ suc 𝑗)
88	87	sscond 4120	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏))
89		intss 4899	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏) → ∩ (𝑆 ∖ suc 𝑏) ⊆ ∩ (𝑆 ∖ suc 𝑗))
90	88, 89	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → ∩ (𝑆 ∖ suc 𝑏) ⊆ ∩ (𝑆 ∖ suc 𝑗))
91		simpl2 1188	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑆 ⊆ On)
92		ordelon 6217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Ord suc 𝑗 ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
93	84, 92	sylan 582	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
94		onmindif 6282	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ⊆ On ∧ 𝑏 ∈ On) → 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑏))
95	91, 93, 94	syl2anc 586	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑏))
96	90, 95	sseldd 3970	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗))
97	83, 96	impbida 799	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗))
98	68, 70, 73, 97	syl3anc 1367	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗))
99		df-suc 6199	. . . . . . . . . . . . . . . 16 ⊢ suc 𝑗 = (𝑗 ∪ {𝑗})
100	99	eleq2i 2906	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ suc 𝑗 ↔ 𝑏 ∈ (𝑗 ∪ {𝑗}))
101	98, 100	syl6bb 289	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗})))
102	101	expr 459	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑏 ∈ 𝑆 → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗}))))
103	102	pm5.32rd 580	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ∧ 𝑏 ∈ 𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏 ∈ 𝑆)))
104		elin 4171	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ∧ 𝑏 ∈ 𝑆))
105		elin 4171	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏 ∈ 𝑆))
106	103, 104, 105	3bitr4g 316	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑏 ∈ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ 𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆)))
107	106	eqrdv 2821	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∪ {𝑗}) ∩ 𝑆))
108		indir 4254	. . . . . . . . . 10 ⊢ ((𝑗 ∪ {𝑗}) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆))
109	107, 108	syl6eq 2874	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)))
110		snssi 4743	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ 𝑆 → {𝑗} ⊆ 𝑆)
111		df-ss 3954	. . . . . . . . . . . 12 ⊢ ({𝑗} ⊆ 𝑆 ↔ ({𝑗} ∩ 𝑆) = {𝑗})
112	110, 111	sylib 220	. . . . . . . . . . 11 ⊢ (𝑗 ∈ 𝑆 → ({𝑗} ∩ 𝑆) = {𝑗})
113	112	uneq2d 4141	. . . . . . . . . 10 ⊢ (𝑗 ∈ 𝑆 → ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗 ∩ 𝑆) ∪ {𝑗}))
114	113	ad2antrl 726	. . . . . . . . 9 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗 ∩ 𝑆) ∪ {𝑗}))
115	109, 114	eqtrd 2858	. . . . . . . 8 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ {𝑗}))
116		df-suc 6199	. . . . . . . . 9 ⊢ suc 𝑎 = (𝑎 ∪ {𝑎})
117	116	a1i 11	. . . . . . . 8 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → suc 𝑎 = (𝑎 ∪ {𝑎}))
118	67, 115, 117	3brtr4d 5100	. . . . . . 7 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎)
119		ineq1 4183	. . . . . . . . 9 ⊢ (𝑏 = ∩ (𝑆 ∖ suc 𝑗) → (𝑏 ∩ 𝑆) = (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆))
120	119	breq1d 5078	. . . . . . . 8 ⊢ (𝑏 = ∩ (𝑆 ∖ suc 𝑗) → ((𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎))
121	120	rspcev 3625	. . . . . . 7 ⊢ ((∩ (𝑆 ∖ suc 𝑗) ∈ 𝑆 ∧ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎) → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎)
122	45, 118, 121	syl2anc 586	. . . . . 6 ⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎)
123	122	rexlimdvaa 3287	. . . . 5 ⊢ ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎))
124		ineq1 4183	. . . . . . 7 ⊢ (𝑏 = 𝑗 → (𝑏 ∩ 𝑆) = (𝑗 ∩ 𝑆))
125	124	breq1d 5078	. . . . . 6 ⊢ (𝑏 = 𝑗 → ((𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ (𝑗 ∩ 𝑆) ≈ suc 𝑎))
126	125	cbvrexvw 3452	. . . . 5 ⊢ (∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎)
127	123, 126	syl6ib 253	. . . 4 ⊢ ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎))
128	127	ex 415	. . 3 ⊢ (𝑎 ∈ ω → ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎)))
129	2, 4, 6, 21, 128	finds2 7612	. 2 ⊢ (𝑖 ∈ ω → ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖))
130	129	impcom 410	1 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   ≠ wne 3018  ∃wrex 3141  Vcvv 3496   ∖ cdif 3935   ∪ cun 3936   ∩ cin 3937   ⊆ wss 3938  ∅c0 4293  {csn 4569  ∩ cint 4878   class class class wbr 5068  Ord word 6192  Oncon0 6193  suc csuc 6195  ωcom 7582   ≈ cen 8508  Fincfn 8511

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-int 4879  df-br 5069  df-opab 5131  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-om 7583  df-1o 8104  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-fin 8515

This theorem is referenced by:  fin23lem23  9750