ackbij1lem16 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ackbij1lem16		Structured version Visualization version GIF version

Theorem ackbij1lem16 8940

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

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

**Assertion**
Ref	Expression
ackbij1lem16	⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘𝐴) = (𝐹‘𝐵) → 𝐴 = 𝐵))

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

Proof of Theorem ackbij1lem16 Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		inss1 3795	. . . . . . . . 9 ⊢ (𝒫 ω ∩ Fin) ⊆ 𝒫 ω
2	1	sseli 3564	. . . . . . . 8 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → 𝐴 ∈ 𝒫 ω)
3	2	elpwid 4118	. . . . . . 7 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → 𝐴 ⊆ ω)
4	3	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐴 ⊆ ω)
5	1	sseli 3564	. . . . . . . 8 ⊢ (𝐵 ∈ (𝒫 ω ∩ Fin) → 𝐵 ∈ 𝒫 ω)
6	5	elpwid 4118	. . . . . . 7 ⊢ (𝐵 ∈ (𝒫 ω ∩ Fin) → 𝐵 ⊆ ω)
7	6	adantl 481	. . . . . 6 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐵 ⊆ ω)
8	4, 7	unssd 3751	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ⊆ ω)
9		inss2 3796	. . . . . . 7 ⊢ (𝒫 ω ∩ Fin) ⊆ Fin
10	9	sseli 3564	. . . . . 6 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → 𝐴 ∈ Fin)
11	9	sseli 3564	. . . . . 6 ⊢ (𝐵 ∈ (𝒫 ω ∩ Fin) → 𝐵 ∈ Fin)
12		unfi 8112	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)
13	10, 11, 12	syl2an 493	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ∈ Fin)
14		nnunifi 8096	. . . . 5 ⊢ (((𝐴 ∪ 𝐵) ⊆ ω ∧ (𝐴 ∪ 𝐵) ∈ Fin) → ∪ (𝐴 ∪ 𝐵) ∈ ω)
15	8, 13, 14	syl2anc 691	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ∪ (𝐴 ∪ 𝐵) ∈ ω)
16		peano2 6978	. . . 4 ⊢ (∪ (𝐴 ∪ 𝐵) ∈ ω → suc ∪ (𝐴 ∪ 𝐵) ∈ ω)
17	15, 16	syl 17	. . 3 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → suc ∪ (𝐴 ∪ 𝐵) ∈ ω)
18		ineq2 3770	. . . . . . . 8 ⊢ (𝑎 = ∅ → (𝐴 ∩ 𝑎) = (𝐴 ∩ ∅))
19	18	fveq2d 6107	. . . . . . 7 ⊢ (𝑎 = ∅ → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ ∅)))
20		ineq2 3770	. . . . . . . 8 ⊢ (𝑎 = ∅ → (𝐵 ∩ 𝑎) = (𝐵 ∩ ∅))
21	20	fveq2d 6107	. . . . . . 7 ⊢ (𝑎 = ∅ → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ ∅)))
22	19, 21	eqeq12d 2625	. . . . . 6 ⊢ (𝑎 = ∅ → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅))))
23	18, 20	eqeq12d 2625	. . . . . 6 ⊢ (𝑎 = ∅ → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ ∅) = (𝐵 ∩ ∅)))
24	22, 23	imbi12d 333	. . . . 5 ⊢ (𝑎 = ∅ → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅)) → (𝐴 ∩ ∅) = (𝐵 ∩ ∅))))
25	24	imbi2d 329	. . . 4 ⊢ (𝑎 = ∅ → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅)) → (𝐴 ∩ ∅) = (𝐵 ∩ ∅)))))
26		ineq2 3770	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (𝐴 ∩ 𝑎) = (𝐴 ∩ 𝑏))
27	26	fveq2d 6107	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ 𝑏)))
28		ineq2 3770	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (𝐵 ∩ 𝑎) = (𝐵 ∩ 𝑏))
29	28	fveq2d 6107	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑏)))
30	27, 29	eqeq12d 2625	. . . . . 6 ⊢ (𝑎 = 𝑏 → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
31	26, 28	eqeq12d 2625	. . . . . 6 ⊢ (𝑎 = 𝑏 → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)))
32	30, 31	imbi12d 333	. . . . 5 ⊢ (𝑎 = 𝑏 → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏))))
33	32	imbi2d 329	. . . 4 ⊢ (𝑎 = 𝑏 → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)))))
34		ineq2 3770	. . . . . . . 8 ⊢ (𝑎 = suc 𝑏 → (𝐴 ∩ 𝑎) = (𝐴 ∩ suc 𝑏))
35	34	fveq2d 6107	. . . . . . 7 ⊢ (𝑎 = suc 𝑏 → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
36		ineq2 3770	. . . . . . . 8 ⊢ (𝑎 = suc 𝑏 → (𝐵 ∩ 𝑎) = (𝐵 ∩ suc 𝑏))
37	36	fveq2d 6107	. . . . . . 7 ⊢ (𝑎 = suc 𝑏 → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
38	35, 37	eqeq12d 2625	. . . . . 6 ⊢ (𝑎 = suc 𝑏 → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))))
39	34, 36	eqeq12d 2625	. . . . . 6 ⊢ (𝑎 = suc 𝑏 → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
40	38, 39	imbi12d 333	. . . . 5 ⊢ (𝑎 = suc 𝑏 → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))))
41	40	imbi2d 329	. . . 4 ⊢ (𝑎 = suc 𝑏 → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
42		ineq2 3770	. . . . . . . 8 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐴 ∩ 𝑎) = (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)))
43	42	fveq2d 6107	. . . . . . 7 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))))
44		ineq2 3770	. . . . . . . 8 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐵 ∩ 𝑎) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))
45	44	fveq2d 6107	. . . . . . 7 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))
46	43, 45	eqeq12d 2625	. . . . . 6 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))))
47	42, 44	eqeq12d 2625	. . . . . 6 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))
48	46, 47	imbi12d 333	. . . . 5 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))))
49	48	imbi2d 329	. . . 4 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))))
50		in0 3920	. . . . . 6 ⊢ (𝐴 ∩ ∅) = ∅
51		in0 3920	. . . . . 6 ⊢ (𝐵 ∩ ∅) = ∅
52	50, 51	eqtr4i 2635	. . . . 5 ⊢ (𝐴 ∩ ∅) = (𝐵 ∩ ∅)
53	52	2a1i 12	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅)) → (𝐴 ∩ ∅) = (𝐵 ∩ ∅)))
54		simp13 1086	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
55		3simpa 1051	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))))
56		ackbij1lem2 8926	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ 𝐴 → (𝐴 ∩ suc 𝑏) = ({𝑏} ∪ (𝐴 ∩ 𝑏)))
57	56	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ 𝐴 → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))))
58	57	3ad2ant2 1076	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))))
59		ackbij1lem4 8928	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ ω → {𝑏} ∈ (𝒫 ω ∩ Fin))
60	59	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → {𝑏} ∈ (𝒫 ω ∩ Fin))
61		simprl 790	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → 𝐴 ∈ (𝒫 ω ∩ Fin))
62		inss1 3795	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∩ 𝑏) ⊆ 𝐴
63		ackbij.f	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))
64	63	ackbij1lem11 8935	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝑏) ⊆ 𝐴) → (𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
65	61, 62, 64	sylancl 693	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
66		incom 3767	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑏} ∩ (𝐴 ∩ 𝑏)) = ((𝐴 ∩ 𝑏) ∩ {𝑏})
67		inss2 3796	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∩ 𝑏) ⊆ 𝑏
68		nnord 6965	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ ω → Ord 𝑏)
69		orddisj 5679	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Ord 𝑏 → (𝑏 ∩ {𝑏}) = ∅)
70	68, 69	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ ω → (𝑏 ∩ {𝑏}) = ∅)
71	70	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝑏 ∩ {𝑏}) = ∅)
72		ssdisj 3978	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∩ 𝑏) ⊆ 𝑏 ∧ (𝑏 ∩ {𝑏}) = ∅) → ((𝐴 ∩ 𝑏) ∩ {𝑏}) = ∅)
73	67, 71, 72	sylancr 694	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ((𝐴 ∩ 𝑏) ∩ {𝑏}) = ∅)
74	66, 73	syl5eq 2656	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ({𝑏} ∩ (𝐴 ∩ 𝑏)) = ∅)
75	63	ackbij1lem9 8933	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑏} ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) ∧ ({𝑏} ∩ (𝐴 ∩ 𝑏)) = ∅) → (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐴 ∩ 𝑏))))
76	60, 65, 74, 75	syl3anc 1318	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐴 ∩ 𝑏))))
77	76	3ad2ant1 1075	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐴 ∩ 𝑏))))
78	58, 77	eqtrd 2644	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐴 ∩ 𝑏))))
79	55, 78	syl3an1 1351	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐴 ∩ 𝑏))))
80		ackbij1lem2 8926	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ 𝐵 → (𝐵 ∩ suc 𝑏) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
81	80	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ 𝐵 → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))))
82	81	3ad2ant3 1077	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))))
83		simprr 792	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → 𝐵 ∈ (𝒫 ω ∩ Fin))
84		inss1 3795	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∩ 𝑏) ⊆ 𝐵
85	63	ackbij1lem11 8935	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ (𝒫 ω ∩ Fin) ∧ (𝐵 ∩ 𝑏) ⊆ 𝐵) → (𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
86	83, 84, 85	sylancl 693	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
87		incom 3767	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑏} ∩ (𝐵 ∩ 𝑏)) = ((𝐵 ∩ 𝑏) ∩ {𝑏})
88		inss2 3796	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∩ 𝑏) ⊆ 𝑏
89		ssdisj 3978	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 ∩ 𝑏) ⊆ 𝑏 ∧ (𝑏 ∩ {𝑏}) = ∅) → ((𝐵 ∩ 𝑏) ∩ {𝑏}) = ∅)
90	88, 71, 89	sylancr 694	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ((𝐵 ∩ 𝑏) ∩ {𝑏}) = ∅)
91	87, 90	syl5eq 2656	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ({𝑏} ∩ (𝐵 ∩ 𝑏)) = ∅)
92	63	ackbij1lem9 8933	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑏} ∈ (𝒫 ω ∩ Fin) ∧ (𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) ∧ ({𝑏} ∩ (𝐵 ∩ 𝑏)) = ∅) → (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐵 ∩ 𝑏))))
93	60, 86, 91, 92	syl3anc 1318	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐵 ∩ 𝑏))))
94	93	3ad2ant1 1075	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐵 ∩ 𝑏))))
95	82, 94	eqtrd 2644	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐵 ∩ 𝑏))))
96	55, 95	syl3an1 1351	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐵 ∩ 𝑏))))
97	54, 79, 96	3eqtr3d 2652	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐵 ∩ 𝑏))))
98	63	ackbij1lem10 8934	. . . . . . . . . . . . . . . . 17 ⊢ 𝐹:(𝒫 ω ∩ Fin)⟶ω
99	98	ffvelrni 6266	. . . . . . . . . . . . . . . 16 ⊢ ({𝑏} ∈ (𝒫 ω ∩ Fin) → (𝐹‘{𝑏}) ∈ ω)
100	60, 99	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘{𝑏}) ∈ ω)
101	98	ffvelrni 6266	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) → (𝐹‘(𝐴 ∩ 𝑏)) ∈ ω)
102	65, 101	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘(𝐴 ∩ 𝑏)) ∈ ω)
103	98	ffvelrni 6266	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) → (𝐹‘(𝐵 ∩ 𝑏)) ∈ ω)
104	86, 103	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘(𝐵 ∩ 𝑏)) ∈ ω)
105		nnacan 7595	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘{𝑏}) ∈ ω ∧ (𝐹‘(𝐴 ∩ 𝑏)) ∈ ω ∧ (𝐹‘(𝐵 ∩ 𝑏)) ∈ ω) → (((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
106	100, 102, 104, 105	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
107	106	3adant3 1074	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
108	107	3ad2ant1 1075	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_𝑜 (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
109	97, 108	mpbid 221	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)))
110		uneq2 3723	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → ({𝑏} ∪ (𝐴 ∩ 𝑏)) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
111	110	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → ({𝑏} ∪ (𝐴 ∩ 𝑏)) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
112	56	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = ({𝑏} ∪ (𝐴 ∩ 𝑏)))
113	80	ad2antlr 759	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐵 ∩ suc 𝑏) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
114	111, 112, 113	3eqtr4d 2654	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))
115	114	ex 449	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
116	115	3adant1 1072	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
117	109, 116	embantd 57	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
118	117	3exp 1256	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ 𝐴 → (𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
119		simp13 1086	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
120	119	eqcomd 2616	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
121		simp12r 1168	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐵 ∈ (𝒫 ω ∩ Fin))
122		simp12l 1167	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐴 ∈ (𝒫 ω ∩ Fin))
123		simp11 1084	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ ω)
124		simp3 1056	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
125		simp2 1055	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ¬ 𝑏 ∈ 𝐴)
126	63	ackbij1lem15 8939	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ (𝒫 ω ∩ Fin) ∧ 𝐴 ∈ (𝒫 ω ∩ Fin)) ∧ (𝑏 ∈ ω ∧ 𝑏 ∈ 𝐵 ∧ ¬ 𝑏 ∈ 𝐴)) → ¬ (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
127	121, 122, 123, 124, 125, 126	syl23anc 1325	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ¬ (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
128	120, 127	pm2.21dd 185	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
129	128	3exp 1256	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (¬ 𝑏 ∈ 𝐴 → (𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
130	118, 129	pm2.61d 169	. . . . . . . 8 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))))
131		simp13 1086	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
132		simp12l 1167	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝐴 ∈ (𝒫 ω ∩ Fin))
133		simp12r 1168	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝐵 ∈ (𝒫 ω ∩ Fin))
134		simp11 1084	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝑏 ∈ ω)
135		simp2 1055	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐴)
136		simp3 1056	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ¬ 𝑏 ∈ 𝐵)
137	63	ackbij1lem15 8939	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝑏 ∈ ω ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵)) → ¬ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
138	132, 133, 134, 135, 136, 137	syl23anc 1325	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ¬ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
139	131, 138	pm2.21dd 185	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
140	139	3exp 1256	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ 𝐴 → (¬ 𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
141		simp13 1086	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
142		ackbij1lem1 8925	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑏 ∈ 𝐴 → (𝐴 ∩ suc 𝑏) = (𝐴 ∩ 𝑏))
143	142	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐴 ∩ suc 𝑏) = (𝐴 ∩ 𝑏))
144	143	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ 𝑏)))
145		ackbij1lem1 8925	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑏 ∈ 𝐵 → (𝐵 ∩ suc 𝑏) = (𝐵 ∩ 𝑏))
146	145	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐵 ∩ suc 𝑏) = (𝐵 ∩ 𝑏))
147	146	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)))
148	144, 147	eqeq12d 2625	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
149	148	biimpd 218	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
150	149	3adant1 1072	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
151	141, 150	mpd 15	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)))
152	143, 146	eqeq12d 2625	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏) ↔ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)))
153	152	biimprd 237	. . . . . . . . . . . 12 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
154	153	3adant1 1072	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
155	151, 154	embantd 57	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
156	155	3exp 1256	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (¬ 𝑏 ∈ 𝐴 → (¬ 𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
157	140, 156	pm2.61d 169	. . . . . . . 8 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (¬ 𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))))
158	130, 157	pm2.61d 169	. . . . . . 7 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
159	158	3exp 1256	. . . . . 6 ⊢ (𝑏 ∈ ω → ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
160	159	com34 89	. . . . 5 ⊢ (𝑏 ∈ ω → ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
161	160	a2d 29	. . . 4 ⊢ (𝑏 ∈ ω → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏))) → ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
162	25, 33, 41, 49, 53, 161	finds 6984	. . 3 ⊢ (suc ∪ (𝐴 ∪ 𝐵) ∈ ω → ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))))
163	17, 162	mpcom 37	. 2 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))
164		omsson 6961	. . . . . . . 8 ⊢ ω ⊆ On
165	8, 164	syl6ss 3580	. . . . . . 7 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ⊆ On)
166		onsucuni 6920	. . . . . . 7 ⊢ ((𝐴 ∪ 𝐵) ⊆ On → (𝐴 ∪ 𝐵) ⊆ suc ∪ (𝐴 ∪ 𝐵))
167	165, 166	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ⊆ suc ∪ (𝐴 ∪ 𝐵))
168	167	unssad 3752	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐴 ⊆ suc ∪ (𝐴 ∪ 𝐵))
169		df-ss 3554	. . . . 5 ⊢ (𝐴 ⊆ suc ∪ (𝐴 ∪ 𝐵) ↔ (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐴)
170	168, 169	sylib 207	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐴)
171	170	fveq2d 6107	. . 3 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘𝐴))
172	167	unssbd 3753	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐵 ⊆ suc ∪ (𝐴 ∪ 𝐵))
173		df-ss 3554	. . . . 5 ⊢ (𝐵 ⊆ suc ∪ (𝐴 ∪ 𝐵) ↔ (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐵)
174	172, 173	sylib 207	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐵)
175	174	fveq2d 6107	. . 3 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘𝐵))
176	171, 175	eqeq12d 2625	. 2 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) ↔ (𝐹‘𝐴) = (𝐹‘𝐵)))
177	170, 174	eqeq12d 2625	. 2 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)) ↔ 𝐴 = 𝐵))
178	163, 176, 177	3imtr3d 281	1 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘𝐴) = (𝐹‘𝐵) → 𝐴 = 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ∪ cun 3538 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 𝒫 cpw 4108 {csn 4125 ∪ cuni 4372 ∪ ciun 4455 ↦ cmpt 4643 × cxp 5036 Ord word 5639 Oncon0 5640 suc csuc 5642 ‘cfv 5804 (class class class)co 6549 ωcom 6957 +_𝑜 coa 7444 Fincfn 7841 cardccrd 8644

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-map 7746 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-cda 8873

This theorem is referenced by: ackbij1lem17 8941

W3C validator