Theorem ackbij1lem16 9651

Description: Lemma for ackbij1 9654. (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 4205	. . . . . . . . 9 ⊢ (𝒫 ω ∩ Fin) ⊆ 𝒫 ω
2	1	sseli 3963	. . . . . . . 8 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → 𝐴 ∈ 𝒫 ω)
3	2	elpwid 4553	. . . . . . 7 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → 𝐴 ⊆ ω)
4	3	adantr 483	. . . . . 6 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐴 ⊆ ω)
5	1	sseli 3963	. . . . . . . 8 ⊢ (𝐵 ∈ (𝒫 ω ∩ Fin) → 𝐵 ∈ 𝒫 ω)
6	5	elpwid 4553	. . . . . . 7 ⊢ (𝐵 ∈ (𝒫 ω ∩ Fin) → 𝐵 ⊆ ω)
7	6	adantl 484	. . . . . 6 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐵 ⊆ ω)
8	4, 7	unssd 4162	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ⊆ ω)
9		inss2 4206	. . . . . . 7 ⊢ (𝒫 ω ∩ Fin) ⊆ Fin
10	9	sseli 3963	. . . . . 6 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → 𝐴 ∈ Fin)
11	9	sseli 3963	. . . . . 6 ⊢ (𝐵 ∈ (𝒫 ω ∩ Fin) → 𝐵 ∈ Fin)
12		unfi 8779	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)
13	10, 11, 12	syl2an 597	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ∈ Fin)
14		nnunifi 8763	. . . . 5 ⊢ (((𝐴 ∪ 𝐵) ⊆ ω ∧ (𝐴 ∪ 𝐵) ∈ Fin) → ∪ (𝐴 ∪ 𝐵) ∈ ω)
15	8, 13, 14	syl2anc 586	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ∪ (𝐴 ∪ 𝐵) ∈ ω)
16		peano2 7596	. . . 4 ⊢ (∪ (𝐴 ∪ 𝐵) ∈ ω → suc ∪ (𝐴 ∪ 𝐵) ∈ ω)
17	15, 16	syl 17	. . 3 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → suc ∪ (𝐴 ∪ 𝐵) ∈ ω)
18		ineq2 4183	. . . . . . . 8 ⊢ (𝑎 = ∅ → (𝐴 ∩ 𝑎) = (𝐴 ∩ ∅))
19	18	fveq2d 6669	. . . . . . 7 ⊢ (𝑎 = ∅ → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ ∅)))
20		ineq2 4183	. . . . . . . 8 ⊢ (𝑎 = ∅ → (𝐵 ∩ 𝑎) = (𝐵 ∩ ∅))
21	20	fveq2d 6669	. . . . . . 7 ⊢ (𝑎 = ∅ → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ ∅)))
22	19, 21	eqeq12d 2837	. . . . . 6 ⊢ (𝑎 = ∅ → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅))))
23	18, 20	eqeq12d 2837	. . . . . 6 ⊢ (𝑎 = ∅ → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ ∅) = (𝐵 ∩ ∅)))
24	22, 23	imbi12d 347	. . . . 5 ⊢ (𝑎 = ∅ → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅)) → (𝐴 ∩ ∅) = (𝐵 ∩ ∅))))
25	24	imbi2d 343	. . . 4 ⊢ (𝑎 = ∅ → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅)) → (𝐴 ∩ ∅) = (𝐵 ∩ ∅)))))
26		ineq2 4183	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (𝐴 ∩ 𝑎) = (𝐴 ∩ 𝑏))
27	26	fveq2d 6669	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ 𝑏)))
28		ineq2 4183	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (𝐵 ∩ 𝑎) = (𝐵 ∩ 𝑏))
29	28	fveq2d 6669	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑏)))
30	27, 29	eqeq12d 2837	. . . . . 6 ⊢ (𝑎 = 𝑏 → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
31	26, 28	eqeq12d 2837	. . . . . 6 ⊢ (𝑎 = 𝑏 → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)))
32	30, 31	imbi12d 347	. . . . 5 ⊢ (𝑎 = 𝑏 → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏))))
33	32	imbi2d 343	. . . 4 ⊢ (𝑎 = 𝑏 → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)))))
34		ineq2 4183	. . . . . . . 8 ⊢ (𝑎 = suc 𝑏 → (𝐴 ∩ 𝑎) = (𝐴 ∩ suc 𝑏))
35	34	fveq2d 6669	. . . . . . 7 ⊢ (𝑎 = suc 𝑏 → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
36		ineq2 4183	. . . . . . . 8 ⊢ (𝑎 = suc 𝑏 → (𝐵 ∩ 𝑎) = (𝐵 ∩ suc 𝑏))
37	36	fveq2d 6669	. . . . . . 7 ⊢ (𝑎 = suc 𝑏 → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
38	35, 37	eqeq12d 2837	. . . . . 6 ⊢ (𝑎 = suc 𝑏 → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))))
39	34, 36	eqeq12d 2837	. . . . . 6 ⊢ (𝑎 = suc 𝑏 → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
40	38, 39	imbi12d 347	. . . . 5 ⊢ (𝑎 = suc 𝑏 → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))))
41	40	imbi2d 343	. . . 4 ⊢ (𝑎 = suc 𝑏 → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
42		ineq2 4183	. . . . . . . 8 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐴 ∩ 𝑎) = (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)))
43	42	fveq2d 6669	. . . . . . 7 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))))
44		ineq2 4183	. . . . . . . 8 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐵 ∩ 𝑎) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))
45	44	fveq2d 6669	. . . . . . 7 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))
46	43, 45	eqeq12d 2837	. . . . . 6 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))))
47	42, 44	eqeq12d 2837	. . . . . 6 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))
48	46, 47	imbi12d 347	. . . . 5 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))))
49	48	imbi2d 343	. . . 4 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))))
50		in0 4345	. . . . . 6 ⊢ (𝐴 ∩ ∅) = ∅
51		in0 4345	. . . . . 6 ⊢ (𝐵 ∩ ∅) = ∅
52	50, 51	eqtr4i 2847	. . . . 5 ⊢ (𝐴 ∩ ∅) = (𝐵 ∩ ∅)
53	52	2a1i 12	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅)) → (𝐴 ∩ ∅) = (𝐵 ∩ ∅)))
54		simp13 1201	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
55		3simpa 1144	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))))
56		ackbij1lem2 9637	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ 𝐴 → (𝐴 ∩ suc 𝑏) = ({𝑏} ∪ (𝐴 ∩ 𝑏)))
57	56	fveq2d 6669	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ 𝐴 → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))))
58	57	3ad2ant2 1130	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))))
59		ackbij1lem4 9639	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ ω → {𝑏} ∈ (𝒫 ω ∩ Fin))
60	59	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → {𝑏} ∈ (𝒫 ω ∩ Fin))
61		simprl 769	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → 𝐴 ∈ (𝒫 ω ∩ Fin))
62		inss1 4205	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∩ 𝑏) ⊆ 𝐴
63		ackbij.f	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))
64	63	ackbij1lem11 9646	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝑏) ⊆ 𝐴) → (𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
65	61, 62, 64	sylancl 588	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
66		incom 4178	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑏} ∩ (𝐴 ∩ 𝑏)) = ((𝐴 ∩ 𝑏) ∩ {𝑏})
67		inss2 4206	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∩ 𝑏) ⊆ 𝑏
68		nnord 7582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ ω → Ord 𝑏)
69		orddisj 6224	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Ord 𝑏 → (𝑏 ∩ {𝑏}) = ∅)
70	68, 69	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ ω → (𝑏 ∩ {𝑏}) = ∅)
71	70	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝑏 ∩ {𝑏}) = ∅)
72		ssdisj 4409	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∩ 𝑏) ⊆ 𝑏 ∧ (𝑏 ∩ {𝑏}) = ∅) → ((𝐴 ∩ 𝑏) ∩ {𝑏}) = ∅)
73	67, 71, 72	sylancr 589	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ((𝐴 ∩ 𝑏) ∩ {𝑏}) = ∅)
74	66, 73	syl5eq 2868	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ({𝑏} ∩ (𝐴 ∩ 𝑏)) = ∅)
75	63	ackbij1lem9 9644	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑏} ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) ∧ ({𝑏} ∩ (𝐴 ∩ 𝑏)) = ∅) → (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +o (𝐹‘(𝐴 ∩ 𝑏))))
76	60, 65, 74, 75	syl3anc 1367	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +o (𝐹‘(𝐴 ∩ 𝑏))))
77	76	3ad2ant1 1129	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +o (𝐹‘(𝐴 ∩ 𝑏))))
78	58, 77	eqtrd 2856	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +o (𝐹‘(𝐴 ∩ 𝑏))))
79	55, 78	syl3an1 1159	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +o (𝐹‘(𝐴 ∩ 𝑏))))
80		ackbij1lem2 9637	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ 𝐵 → (𝐵 ∩ suc 𝑏) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
81	80	fveq2d 6669	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ 𝐵 → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))))
82	81	3ad2ant3 1131	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))))
83		simprr 771	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → 𝐵 ∈ (𝒫 ω ∩ Fin))
84		inss1 4205	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∩ 𝑏) ⊆ 𝐵
85	63	ackbij1lem11 9646	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ (𝒫 ω ∩ Fin) ∧ (𝐵 ∩ 𝑏) ⊆ 𝐵) → (𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
86	83, 84, 85	sylancl 588	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
87		incom 4178	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑏} ∩ (𝐵 ∩ 𝑏)) = ((𝐵 ∩ 𝑏) ∩ {𝑏})
88		inss2 4206	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∩ 𝑏) ⊆ 𝑏
89		ssdisj 4409	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 ∩ 𝑏) ⊆ 𝑏 ∧ (𝑏 ∩ {𝑏}) = ∅) → ((𝐵 ∩ 𝑏) ∩ {𝑏}) = ∅)
90	88, 71, 89	sylancr 589	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ((𝐵 ∩ 𝑏) ∩ {𝑏}) = ∅)
91	87, 90	syl5eq 2868	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ({𝑏} ∩ (𝐵 ∩ 𝑏)) = ∅)
92	63	ackbij1lem9 9644	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑏} ∈ (𝒫 ω ∩ Fin) ∧ (𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) ∧ ({𝑏} ∩ (𝐵 ∩ 𝑏)) = ∅) → (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))) = ((𝐹‘{𝑏}) +o (𝐹‘(𝐵 ∩ 𝑏))))
93	60, 86, 91, 92	syl3anc 1367	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))) = ((𝐹‘{𝑏}) +o (𝐹‘(𝐵 ∩ 𝑏))))
94	93	3ad2ant1 1129	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))) = ((𝐹‘{𝑏}) +o (𝐹‘(𝐵 ∩ 𝑏))))
95	82, 94	eqtrd 2856	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +o (𝐹‘(𝐵 ∩ 𝑏))))
96	55, 95	syl3an1 1159	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +o (𝐹‘(𝐵 ∩ 𝑏))))
97	54, 79, 96	3eqtr3d 2864	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((𝐹‘{𝑏}) +o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +o (𝐹‘(𝐵 ∩ 𝑏))))
98	63	ackbij1lem10 9645	. . . . . . . . . . . . . . . . 17 ⊢ 𝐹:(𝒫 ω ∩ Fin)⟶ω
99	98	ffvelrni 6845	. . . . . . . . . . . . . . . 16 ⊢ ({𝑏} ∈ (𝒫 ω ∩ Fin) → (𝐹‘{𝑏}) ∈ ω)
100	60, 99	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘{𝑏}) ∈ ω)
101	98	ffvelrni 6845	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) → (𝐹‘(𝐴 ∩ 𝑏)) ∈ ω)
102	65, 101	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘(𝐴 ∩ 𝑏)) ∈ ω)
103	98	ffvelrni 6845	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) → (𝐹‘(𝐵 ∩ 𝑏)) ∈ ω)
104	86, 103	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘(𝐵 ∩ 𝑏)) ∈ ω)
105		nnacan 8248	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘{𝑏}) ∈ ω ∧ (𝐹‘(𝐴 ∩ 𝑏)) ∈ ω ∧ (𝐹‘(𝐵 ∩ 𝑏)) ∈ ω) → (((𝐹‘{𝑏}) +o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +o (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
106	100, 102, 104, 105	syl3anc 1367	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (((𝐹‘{𝑏}) +o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +o (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
107	106	3adant3 1128	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (((𝐹‘{𝑏}) +o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +o (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
108	107	3ad2ant1 1129	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (((𝐹‘{𝑏}) +o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +o (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
109	97, 108	mpbid 234	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)))
110		uneq2 4133	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → ({𝑏} ∪ (𝐴 ∩ 𝑏)) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
111	110	adantl 484	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → ({𝑏} ∪ (𝐴 ∩ 𝑏)) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
112	56	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = ({𝑏} ∪ (𝐴 ∩ 𝑏)))
113	80	ad2antlr 725	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐵 ∩ suc 𝑏) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
114	111, 112, 113	3eqtr4d 2866	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))
115	114	ex 415	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
116	115	3adant1 1126	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
117	109, 116	embantd 59	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
118	117	3exp 1115	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ 𝐴 → (𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
119		simp13 1201	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
120	119	eqcomd 2827	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
121		simp12r 1283	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐵 ∈ (𝒫 ω ∩ Fin))
122		simp12l 1282	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐴 ∈ (𝒫 ω ∩ Fin))
123		simp11 1199	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ ω)
124		simp3 1134	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
125		simp2 1133	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ¬ 𝑏 ∈ 𝐴)
126	63	ackbij1lem15 9650	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ (𝒫 ω ∩ Fin) ∧ 𝐴 ∈ (𝒫 ω ∩ Fin)) ∧ (𝑏 ∈ ω ∧ 𝑏 ∈ 𝐵 ∧ ¬ 𝑏 ∈ 𝐴)) → ¬ (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
127	121, 122, 123, 124, 125, 126	syl23anc 1373	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ¬ (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
128	120, 127	pm2.21dd 197	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
129	128	3exp 1115	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (¬ 𝑏 ∈ 𝐴 → (𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
130	118, 129	pm2.61d 181	. . . . . . . 8 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))))
131		simp13 1201	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
132		simp12l 1282	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝐴 ∈ (𝒫 ω ∩ Fin))
133		simp12r 1283	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝐵 ∈ (𝒫 ω ∩ Fin))
134		simp11 1199	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝑏 ∈ ω)
135		simp2 1133	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐴)
136		simp3 1134	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ¬ 𝑏 ∈ 𝐵)
137	63	ackbij1lem15 9650	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝑏 ∈ ω ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵)) → ¬ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
138	132, 133, 134, 135, 136, 137	syl23anc 1373	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ¬ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
139	131, 138	pm2.21dd 197	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
140	139	3exp 1115	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ 𝐴 → (¬ 𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
141		simp13 1201	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
142		ackbij1lem1 9636	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑏 ∈ 𝐴 → (𝐴 ∩ suc 𝑏) = (𝐴 ∩ 𝑏))
143	142	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐴 ∩ suc 𝑏) = (𝐴 ∩ 𝑏))
144	143	fveq2d 6669	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ 𝑏)))
145		ackbij1lem1 9636	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑏 ∈ 𝐵 → (𝐵 ∩ suc 𝑏) = (𝐵 ∩ 𝑏))
146	145	adantl 484	. . . . . . . . . . . . . . . 16 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐵 ∩ suc 𝑏) = (𝐵 ∩ 𝑏))
147	146	fveq2d 6669	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)))
148	144, 147	eqeq12d 2837	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
149	148	biimpd 231	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
150	149	3adant1 1126	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
151	141, 150	mpd 15	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)))
152	143, 146	eqeq12d 2837	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏) ↔ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)))
153	152	biimprd 250	. . . . . . . . . . . 12 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
154	153	3adant1 1126	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
155	151, 154	embantd 59	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
156	155	3exp 1115	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (¬ 𝑏 ∈ 𝐴 → (¬ 𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
157	140, 156	pm2.61d 181	. . . . . . . 8 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (¬ 𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))))
158	130, 157	pm2.61d 181	. . . . . . 7 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
159	158	3exp 1115	. . . . . 6 ⊢ (𝑏 ∈ ω → ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
160	159	com34 91	. . . . 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 7602	. . 3 ⊢ (suc ∪ (𝐴 ∪ 𝐵) ∈ ω → ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))))
163	17, 162	mpcom 38	. 2 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))
164		omsson 7578	. . . . . . . 8 ⊢ ω ⊆ On
165	8, 164	sstrdi 3979	. . . . . . 7 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ⊆ On)
166		onsucuni 7537	. . . . . . 7 ⊢ ((𝐴 ∪ 𝐵) ⊆ On → (𝐴 ∪ 𝐵) ⊆ suc ∪ (𝐴 ∪ 𝐵))
167	165, 166	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ⊆ suc ∪ (𝐴 ∪ 𝐵))
168	167	unssad 4163	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐴 ⊆ suc ∪ (𝐴 ∪ 𝐵))
169		df-ss 3952	. . . . 5 ⊢ (𝐴 ⊆ suc ∪ (𝐴 ∪ 𝐵) ↔ (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐴)
170	168, 169	sylib 220	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐴)
171	170	fveq2d 6669	. . 3 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘𝐴))
172	167	unssbd 4164	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐵 ⊆ suc ∪ (𝐴 ∪ 𝐵))
173		df-ss 3952	. . . . 5 ⊢ (𝐵 ⊆ suc ∪ (𝐴 ∪ 𝐵) ↔ (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐵)
174	172, 173	sylib 220	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐵)
175	174	fveq2d 6669	. . 3 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘𝐵))
176	171, 175	eqeq12d 2837	. 2 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) ↔ (𝐹‘𝐴) = (𝐹‘𝐵)))
177	170, 174	eqeq12d 2837	. 2 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)) ↔ 𝐴 = 𝐵))
178	163, 176, 177	3imtr3d 295	1 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘𝐴) = (𝐹‘𝐵) → 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110   ∪ cun 3934   ∩ cin 3935   ⊆ wss 3936  ∅c0 4291  𝒫 cpw 4539  {csn 4561  ∪ cuni 4832  ∪ ciun 4912   ↦ cmpt 5139   × cxp 5548  Ord word 6185  Oncon0 6186  suc csuc 6188  ‘cfv 6350  (class class class)co 7150  ωcom 7574   +_o coa 8093  Fincfn 8503  cardccrd 9358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-int 4870  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-tr 5166  df-id 5455  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-we 5511  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-pred 6143  df-ord 6189  df-on 6190  df-lim 6191  df-suc 6192  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-2o 8097  df-oadd 8100  df-er 8283  df-map 8402  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-dju 9324  df-card 9362

This theorem is referenced by:  ackbij1lem17  9652