Theorem ackbij1lem18 10241

Description: Lemma for ackbij1 10242. (Contributed by Stefan O'Rear, 18-Nov-2014.)

Hypothesis

Ref	Expression
ackbij.f	⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))

Assertion

Ref	Expression
ackbij1lem18	⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc (𝐹‘𝐴))

Distinct variable groups:   𝐹,𝑏,𝑥,𝑦   𝐴,𝑏,𝑥,𝑦

Proof of Theorem ackbij1lem18

Dummy variable 𝑎 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		difss 4086	. . . 4 ⊢ (𝐴 ∖ ∩ (ω ∖ 𝐴)) ⊆ 𝐴
2		ackbij.f	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))
3	2	ackbij1lem11 10234	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 ∖ ∩ (ω ∖ 𝐴)) ⊆ 𝐴) → (𝐴 ∖ ∩ (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin))
4	1, 3	mpan2 704	. . 3 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐴 ∖ ∩ (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin))
5		difss 4086	. . . . . . 7 ⊢ (ω ∖ 𝐴) ⊆ ω
6		omsson 7869	. . . . . . 7 ⊢ ω ⊆ On
7	5, 6	sstri 3943	. . . . . 6 ⊢ (ω ∖ 𝐴) ⊆ On
8		ominf 9237	. . . . . . . 8 ⊢ ¬ ω ∈ Fin
9		elinel2 4151	. . . . . . . 8 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → 𝐴 ∈ Fin)
10		difinf 9284	. . . . . . . 8 ⊢ ((¬ ω ∈ Fin ∧ 𝐴 ∈ Fin) → ¬ (ω ∖ 𝐴) ∈ Fin)
11	8, 9, 10	sylancr 599	. . . . . . 7 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ¬ (ω ∖ 𝐴) ∈ Fin)
12		0fi 9052	. . . . . . . . 9 ⊢ ∅ ∈ Fin
13		eleq1 2850	. . . . . . . . 9 ⊢ ((ω ∖ 𝐴) = ∅ → ((ω ∖ 𝐴) ∈ Fin ↔ ∅ ∈ Fin))
14	12, 13	mpbiri 261	. . . . . . . 8 ⊢ ((ω ∖ 𝐴) = ∅ → (ω ∖ 𝐴) ∈ Fin)
15	14	necon3bi 2983	. . . . . . 7 ⊢ (¬ (ω ∖ 𝐴) ∈ Fin → (ω ∖ 𝐴) ≠ ∅)
16	11, 15	syl 18	. . . . . 6 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (ω ∖ 𝐴) ≠ ∅)
17		onint 7792	. . . . . 6 ⊢ (((ω ∖ 𝐴) ⊆ On ∧ (ω ∖ 𝐴) ≠ ∅) → ∩ (ω ∖ 𝐴) ∈ (ω ∖ 𝐴))
18	7, 16, 17	sylancr 599	. . . . 5 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∩ (ω ∖ 𝐴) ∈ (ω ∖ 𝐴))
19	18	eldifad 3914	. . . 4 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∩ (ω ∖ 𝐴) ∈ ω)
20		ackbij1lem4 10227	. . . 4 ⊢ (∩ (ω ∖ 𝐴) ∈ ω → {∩ (ω ∖ 𝐴)} ∈ (𝒫 ω ∩ Fin))
21	19, 20	syl 18	. . 3 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → {∩ (ω ∖ 𝐴)} ∈ (𝒫 ω ∩ Fin))
22		ackbij1lem6 10229	. . 3 ⊢ (((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin) ∧ {∩ (ω ∖ 𝐴)} ∈ (𝒫 ω ∩ Fin)) → ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)}) ∈ (𝒫 ω ∩ Fin))
23	4, 21, 22	syl2anc 596	. 2 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)}) ∈ (𝒫 ω ∩ Fin))
24	18	eldifbd 3915	. . . . . 6 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ¬ ∩ (ω ∖ 𝐴) ∈ 𝐴)
25		disjsn 4675	. . . . . 6 ⊢ ((𝐴 ∩ {∩ (ω ∖ 𝐴)}) = ∅ ↔ ¬ ∩ (ω ∖ 𝐴) ∈ 𝐴)
26	24, 25	sylibr 237	. . . . 5 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐴 ∩ {∩ (ω ∖ 𝐴)}) = ∅)
27		ssdisj 4416	. . . . 5 ⊢ (((𝐴 ∖ ∩ (ω ∖ 𝐴)) ⊆ 𝐴 ∧ (𝐴 ∩ {∩ (ω ∖ 𝐴)}) = ∅) → ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∩ {∩ (ω ∖ 𝐴)}) = ∅)
28	1, 26, 27	sylancr 599	. . . 4 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∩ {∩ (ω ∖ 𝐴)}) = ∅)
29	2	ackbij1lem9 10232	. . . 4 ⊢ (((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin) ∧ {∩ (ω ∖ 𝐴)} ∈ (𝒫 ω ∩ Fin) ∧ ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∩ {∩ (ω ∖ 𝐴)}) = ∅) → (𝐹‘((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)})) = ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +o (𝐹‘{∩ (ω ∖ 𝐴)})))
30	4, 21, 28, 29	syl3anc 1398	. . 3 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)})) = ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +o (𝐹‘{∩ (ω ∖ 𝐴)})))
31	2	ackbij1lem14 10237	. . . . 5 ⊢ (∩ (ω ∖ 𝐴) ∈ ω → (𝐹‘{∩ (ω ∖ 𝐴)}) = suc (𝐹‘∩ (ω ∖ 𝐴)))
32	19, 31	syl 18	. . . 4 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘{∩ (ω ∖ 𝐴)}) = suc (𝐹‘∩ (ω ∖ 𝐴)))
33	32	oveq2d 7432	. . 3 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +o (𝐹‘{∩ (ω ∖ 𝐴)})) = ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +o suc (𝐹‘∩ (ω ∖ 𝐴))))
34	2	ackbij1lem10 10233	. . . . . . 7 ⊢ 𝐹:(𝒫 ω ∩ Fin)⟶ω
35	34	ffvelcdmi 7079	. . . . . 6 ⊢ ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin) → (𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) ∈ ω)
36	4, 35	syl 18	. . . . 5 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) ∈ ω)
37		ackbij1lem3 10226	. . . . . . 7 ⊢ (∩ (ω ∖ 𝐴) ∈ ω → ∩ (ω ∖ 𝐴) ∈ (𝒫 ω ∩ Fin))
38	19, 37	syl 18	. . . . . 6 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∩ (ω ∖ 𝐴) ∈ (𝒫 ω ∩ Fin))
39	34	ffvelcdmi 7079	. . . . . 6 ⊢ (∩ (ω ∖ 𝐴) ∈ (𝒫 ω ∩ Fin) → (𝐹‘∩ (ω ∖ 𝐴)) ∈ ω)
40	38, 39	syl 18	. . . . 5 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘∩ (ω ∖ 𝐴)) ∈ ω)
41		nnasuc 8597	. . . . 5 ⊢ (((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) ∈ ω ∧ (𝐹‘∩ (ω ∖ 𝐴)) ∈ ω) → ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +o suc (𝐹‘∩ (ω ∖ 𝐴))) = suc ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +o (𝐹‘∩ (ω ∖ 𝐴))))
42	36, 40, 41	syl2anc 596	. . . 4 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +o suc (𝐹‘∩ (ω ∖ 𝐴))) = suc ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +o (𝐹‘∩ (ω ∖ 𝐴))))
43		disjdifr 4430	. . . . . . . 8 ⊢ ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∩ ∩ (ω ∖ 𝐴)) = ∅
44	43	a1i 11	. . . . . . 7 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∩ ∩ (ω ∖ 𝐴)) = ∅)
45	2	ackbij1lem9 10232	. . . . . . 7 ⊢ (((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin) ∧ ∩ (ω ∖ 𝐴) ∈ (𝒫 ω ∩ Fin) ∧ ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∩ ∩ (ω ∖ 𝐴)) = ∅) → (𝐹‘((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ ∩ (ω ∖ 𝐴))) = ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +o (𝐹‘∩ (ω ∖ 𝐴))))
46	4, 38, 44, 45	syl3anc 1398	. . . . . 6 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ ∩ (ω ∖ 𝐴))) = ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +o (𝐹‘∩ (ω ∖ 𝐴))))
47		uncom 4108	. . . . . . . 8 ⊢ ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ ∩ (ω ∖ 𝐴)) = (∩ (ω ∖ 𝐴) ∪ (𝐴 ∖ ∩ (ω ∖ 𝐴)))
48		onnmin 7800	. . . . . . . . . . . . . . 15 ⊢ (((ω ∖ 𝐴) ⊆ On ∧ 𝑎 ∈ (ω ∖ 𝐴)) → ¬ 𝑎 ∈ ∩ (ω ∖ 𝐴))
49	7, 48	mpan 703	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (ω ∖ 𝐴) → ¬ 𝑎 ∈ ∩ (ω ∖ 𝐴))
50	49	con2i 140	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ∩ (ω ∖ 𝐴) → ¬ 𝑎 ∈ (ω ∖ 𝐴))
51	50	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝑎 ∈ ∩ (ω ∖ 𝐴)) → ¬ 𝑎 ∈ (ω ∖ 𝐴))
52		ordom 7875	. . . . . . . . . . . . . . 15 ⊢ Ord ω
53		ordelss 6377	. . . . . . . . . . . . . . 15 ⊢ ((Ord ω ∧ ∩ (ω ∖ 𝐴) ∈ ω) → ∩ (ω ∖ 𝐴) ⊆ ω)
54	52, 19, 53	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∩ (ω ∖ 𝐴) ⊆ ω)
55	54	sselda 3934	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝑎 ∈ ∩ (ω ∖ 𝐴)) → 𝑎 ∈ ω)
56		eldif 3912	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (ω ∖ 𝐴) ↔ (𝑎 ∈ ω ∧ ¬ 𝑎 ∈ 𝐴))
57	56	simplbi2 506	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ω → (¬ 𝑎 ∈ 𝐴 → 𝑎 ∈ (ω ∖ 𝐴)))
58	57	orrd 877	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ω → (𝑎 ∈ 𝐴 ∨ 𝑎 ∈ (ω ∖ 𝐴)))
59	58	orcomd 885	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ω → (𝑎 ∈ (ω ∖ 𝐴) ∨ 𝑎 ∈ 𝐴))
60	55, 59	syl 18	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝑎 ∈ ∩ (ω ∖ 𝐴)) → (𝑎 ∈ (ω ∖ 𝐴) ∨ 𝑎 ∈ 𝐴))
61		orel1 902	. . . . . . . . . . . 12 ⊢ (¬ 𝑎 ∈ (ω ∖ 𝐴) → ((𝑎 ∈ (ω ∖ 𝐴) ∨ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐴))
62	51, 60, 61	sylc 66	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝑎 ∈ ∩ (ω ∖ 𝐴)) → 𝑎 ∈ 𝐴)
63	62	ex 418	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝑎 ∈ ∩ (ω ∖ 𝐴) → 𝑎 ∈ 𝐴))
64	63	ssrdv 3940	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∩ (ω ∖ 𝐴) ⊆ 𝐴)
65		undif 4441	. . . . . . . . 9 ⊢ (∩ (ω ∖ 𝐴) ⊆ 𝐴 ↔ (∩ (ω ∖ 𝐴) ∪ (𝐴 ∖ ∩ (ω ∖ 𝐴))) = 𝐴)
66	64, 65	sylib 221	. . . . . . . 8 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (∩ (ω ∖ 𝐴) ∪ (𝐴 ∖ ∩ (ω ∖ 𝐴))) = 𝐴)
67	47, 66	eqtrid 2809	. . . . . . 7 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ ∩ (ω ∖ 𝐴)) = 𝐴)
68	67	fveq2d 6886	. . . . . 6 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ ∩ (ω ∖ 𝐴))) = (𝐹‘𝐴))
69	46, 68	eqtr3d 2799	. . . . 5 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +o (𝐹‘∩ (ω ∖ 𝐴))) = (𝐹‘𝐴))
70		suceq 6430	. . . . 5 ⊢ (((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +o (𝐹‘∩ (ω ∖ 𝐴))) = (𝐹‘𝐴) → suc ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +o (𝐹‘∩ (ω ∖ 𝐴))) = suc (𝐹‘𝐴))
71	69, 70	syl 18	. . . 4 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → suc ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +o (𝐹‘∩ (ω ∖ 𝐴))) = suc (𝐹‘𝐴))
72	42, 71	eqtrd 2797	. . 3 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +o suc (𝐹‘∩ (ω ∖ 𝐴))) = suc (𝐹‘𝐴))
73	30, 33, 72	3eqtrd 2801	. 2 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)})) = suc (𝐹‘𝐴))
74		fveqeq2 6891	. . 3 ⊢ (𝑏 = ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)}) → ((𝐹‘𝑏) = suc (𝐹‘𝐴) ↔ (𝐹‘((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)})) = suc (𝐹‘𝐴)))
75	74	rspcev 3579	. 2 ⊢ ((((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)}) ∈ (𝒫 ω ∩ Fin) ∧ (𝐹‘((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)})) = suc (𝐹‘𝐴)) → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc (𝐹‘𝐴))
76	23, 73, 75	syl2anc 596	1 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc (𝐹‘𝐴))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145   ≠ wne 2957  ∃wrex 3088   ∖ cdif 3899   ∪ cun 3900   ∩ cin 3901   ⊆ wss 3902  ∅c0 4282  𝒫 cpw 4560  {csn 4587  ∩ cint 4910  ∪ ciun 4954   ↦ cmpt 5190   × cxp 5657  Ord word 6360  Oncon0 6361  suc csuc 6363  ‘cfv 6537  (class class class)co 7416  ωcom 7865   +_o coa 8455  Fincfn 8955  cardccrd 9943

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-pow 5334  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-iun 4956  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-pred 6303  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-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7866  df-1st 7989  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8458  df-2o 8459  df-oadd 8462  df-er 8699  df-map 8831  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-dju 9909  df-card 9947

This theorem is used by:  ackbij1  10242