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 9922

Description: Lemma for ackbij1 9925. (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 4159	. . . . . . . . 9 ⊢ (𝒫 ω ∩ Fin) ⊆ 𝒫 ω
2	1	sseli 3913	. . . . . . . 8 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → 𝐴 ∈ 𝒫 ω)
3	2	elpwid 4541	. . . . . . 7 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → 𝐴 ⊆ ω)
4	3	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐴 ⊆ ω)
5	1	sseli 3913	. . . . . . . 8 ⊢ (𝐵 ∈ (𝒫 ω ∩ Fin) → 𝐵 ∈ 𝒫 ω)
6	5	elpwid 4541	. . . . . . 7 ⊢ (𝐵 ∈ (𝒫 ω ∩ Fin) → 𝐵 ⊆ ω)
7	6	adantl 481	. . . . . 6 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐵 ⊆ ω)
8	4, 7	unssd 4116	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ⊆ ω)
9		inss2 4160	. . . . . . 7 ⊢ (𝒫 ω ∩ Fin) ⊆ Fin
10	9	sseli 3913	. . . . . 6 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → 𝐴 ∈ Fin)
11	9	sseli 3913	. . . . . 6 ⊢ (𝐵 ∈ (𝒫 ω ∩ Fin) → 𝐵 ∈ Fin)
12		unfi 8917	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)
13	10, 11, 12	syl2an 595	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ∈ Fin)
14		nnunifi 8995	. . . . 5 ⊢ (((𝐴 ∪ 𝐵) ⊆ ω ∧ (𝐴 ∪ 𝐵) ∈ Fin) → ∪ (𝐴 ∪ 𝐵) ∈ ω)
15	8, 13, 14	syl2anc 583	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ∪ (𝐴 ∪ 𝐵) ∈ ω)
16		peano2 7711	. . . 4 ⊢ (∪ (𝐴 ∪ 𝐵) ∈ ω → suc ∪ (𝐴 ∪ 𝐵) ∈ ω)
17	15, 16	syl 17	. . 3 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → suc ∪ (𝐴 ∪ 𝐵) ∈ ω)
18		ineq2 4137	. . . . . . . 8 ⊢ (𝑎 = ∅ → (𝐴 ∩ 𝑎) = (𝐴 ∩ ∅))
19	18	fveq2d 6760	. . . . . . 7 ⊢ (𝑎 = ∅ → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ ∅)))
20		ineq2 4137	. . . . . . . 8 ⊢ (𝑎 = ∅ → (𝐵 ∩ 𝑎) = (𝐵 ∩ ∅))
21	20	fveq2d 6760	. . . . . . 7 ⊢ (𝑎 = ∅ → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ ∅)))
22	19, 21	eqeq12d 2754	. . . . . 6 ⊢ (𝑎 = ∅ → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅))))
23	18, 20	eqeq12d 2754	. . . . . 6 ⊢ (𝑎 = ∅ → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ ∅) = (𝐵 ∩ ∅)))
24	22, 23	imbi12d 344	. . . . 5 ⊢ (𝑎 = ∅ → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅)) → (𝐴 ∩ ∅) = (𝐵 ∩ ∅))))
25	24	imbi2d 340	. . . 4 ⊢ (𝑎 = ∅ → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅)) → (𝐴 ∩ ∅) = (𝐵 ∩ ∅)))))
26		ineq2 4137	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (𝐴 ∩ 𝑎) = (𝐴 ∩ 𝑏))
27	26	fveq2d 6760	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ 𝑏)))
28		ineq2 4137	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (𝐵 ∩ 𝑎) = (𝐵 ∩ 𝑏))
29	28	fveq2d 6760	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑏)))
30	27, 29	eqeq12d 2754	. . . . . 6 ⊢ (𝑎 = 𝑏 → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
31	26, 28	eqeq12d 2754	. . . . . 6 ⊢ (𝑎 = 𝑏 → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)))
32	30, 31	imbi12d 344	. . . . 5 ⊢ (𝑎 = 𝑏 → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏))))
33	32	imbi2d 340	. . . 4 ⊢ (𝑎 = 𝑏 → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)))))
34		ineq2 4137	. . . . . . . 8 ⊢ (𝑎 = suc 𝑏 → (𝐴 ∩ 𝑎) = (𝐴 ∩ suc 𝑏))
35	34	fveq2d 6760	. . . . . . 7 ⊢ (𝑎 = suc 𝑏 → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
36		ineq2 4137	. . . . . . . 8 ⊢ (𝑎 = suc 𝑏 → (𝐵 ∩ 𝑎) = (𝐵 ∩ suc 𝑏))
37	36	fveq2d 6760	. . . . . . 7 ⊢ (𝑎 = suc 𝑏 → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
38	35, 37	eqeq12d 2754	. . . . . 6 ⊢ (𝑎 = suc 𝑏 → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))))
39	34, 36	eqeq12d 2754	. . . . . 6 ⊢ (𝑎 = suc 𝑏 → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
40	38, 39	imbi12d 344	. . . . 5 ⊢ (𝑎 = suc 𝑏 → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))))
41	40	imbi2d 340	. . . 4 ⊢ (𝑎 = suc 𝑏 → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
42		ineq2 4137	. . . . . . . 8 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐴 ∩ 𝑎) = (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)))
43	42	fveq2d 6760	. . . . . . 7 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))))
44		ineq2 4137	. . . . . . . 8 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐵 ∩ 𝑎) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))
45	44	fveq2d 6760	. . . . . . 7 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (𝐹‘(𝐵 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))
46	43, 45	eqeq12d 2754	. . . . . 6 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) ↔ (𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))))
47	42, 44	eqeq12d 2754	. . . . . 6 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → ((𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎) ↔ (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))
48	46, 47	imbi12d 344	. . . . 5 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎)) ↔ ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))))
49	48	imbi2d 340	. . . 4 ⊢ (𝑎 = suc ∪ (𝐴 ∪ 𝐵) → (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ 𝑎)) = (𝐹‘(𝐵 ∩ 𝑎)) → (𝐴 ∩ 𝑎) = (𝐵 ∩ 𝑎))) ↔ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))))
50		in0 4322	. . . . . 6 ⊢ (𝐴 ∩ ∅) = ∅
51		in0 4322	. . . . . 6 ⊢ (𝐵 ∩ ∅) = ∅
52	50, 51	eqtr4i 2769	. . . . 5 ⊢ (𝐴 ∩ ∅) = (𝐵 ∩ ∅)
53	52	2a1i 12	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ ∅)) = (𝐹‘(𝐵 ∩ ∅)) → (𝐴 ∩ ∅) = (𝐵 ∩ ∅)))
54		simp13 1203	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
55		3simpa 1146	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))))
56		ackbij1lem2 9908	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ 𝐴 → (𝐴 ∩ suc 𝑏) = ({𝑏} ∪ (𝐴 ∩ 𝑏)))
57	56	fveq2d 6760	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ 𝐴 → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))))
58	57	3ad2ant2 1132	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))))
59		ackbij1lem4 9910	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ ω → {𝑏} ∈ (𝒫 ω ∩ Fin))
60	59	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → {𝑏} ∈ (𝒫 ω ∩ Fin))
61		simprl 767	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → 𝐴 ∈ (𝒫 ω ∩ Fin))
62		inss1 4159	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∩ 𝑏) ⊆ 𝐴
63		ackbij.f	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))
64	63	ackbij1lem11 9917	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝑏) ⊆ 𝐴) → (𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
65	61, 62, 64	sylancl 585	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
66		incom 4131	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑏} ∩ (𝐴 ∩ 𝑏)) = ((𝐴 ∩ 𝑏) ∩ {𝑏})
67		inss2 4160	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∩ 𝑏) ⊆ 𝑏
68		nnord 7695	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ ω → Ord 𝑏)
69		orddisj 6289	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Ord 𝑏 → (𝑏 ∩ {𝑏}) = ∅)
70	68, 69	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ ω → (𝑏 ∩ {𝑏}) = ∅)
71	70	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝑏 ∩ {𝑏}) = ∅)
72		ssdisj 4390	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∩ 𝑏) ⊆ 𝑏 ∧ (𝑏 ∩ {𝑏}) = ∅) → ((𝐴 ∩ 𝑏) ∩ {𝑏}) = ∅)
73	67, 71, 72	sylancr 586	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ((𝐴 ∩ 𝑏) ∩ {𝑏}) = ∅)
74	66, 73	eqtrid 2790	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ({𝑏} ∩ (𝐴 ∩ 𝑏)) = ∅)
75	63	ackbij1lem9 9915	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑏} ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) ∧ ({𝑏} ∩ (𝐴 ∩ 𝑏)) = ∅) → (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))))
76	60, 65, 74, 75	syl3anc 1369	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))))
77	76	3ad2ant1 1131	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘({𝑏} ∪ (𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))))
78	58, 77	eqtrd 2778	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))))
79	55, 78	syl3an1 1161	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))))
80		ackbij1lem2 9908	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ 𝐵 → (𝐵 ∩ suc 𝑏) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
81	80	fveq2d 6760	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ 𝐵 → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))))
82	81	3ad2ant3 1133	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))))
83		simprr 769	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → 𝐵 ∈ (𝒫 ω ∩ Fin))
84		inss1 4159	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∩ 𝑏) ⊆ 𝐵
85	63	ackbij1lem11 9917	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ (𝒫 ω ∩ Fin) ∧ (𝐵 ∩ 𝑏) ⊆ 𝐵) → (𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
86	83, 84, 85	sylancl 585	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin))
87		incom 4131	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑏} ∩ (𝐵 ∩ 𝑏)) = ((𝐵 ∩ 𝑏) ∩ {𝑏})
88		inss2 4160	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∩ 𝑏) ⊆ 𝑏
89		ssdisj 4390	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 ∩ 𝑏) ⊆ 𝑏 ∧ (𝑏 ∩ {𝑏}) = ∅) → ((𝐵 ∩ 𝑏) ∩ {𝑏}) = ∅)
90	88, 71, 89	sylancr 586	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ((𝐵 ∩ 𝑏) ∩ {𝑏}) = ∅)
91	87, 90	eqtrid 2790	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → ({𝑏} ∩ (𝐵 ∩ 𝑏)) = ∅)
92	63	ackbij1lem9 9915	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑏} ∈ (𝒫 ω ∩ Fin) ∧ (𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) ∧ ({𝑏} ∩ (𝐵 ∩ 𝑏)) = ∅) → (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))))
93	60, 86, 91, 92	syl3anc 1369	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))))
94	93	3ad2ant1 1131	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘({𝑏} ∪ (𝐵 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))))
95	82, 94	eqtrd 2778	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))))
96	55, 95	syl3an1 1161	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))))
97	54, 79, 96	3eqtr3d 2786	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))))
98	63	ackbij1lem10 9916	. . . . . . . . . . . . . . . . 17 ⊢ 𝐹:(𝒫 ω ∩ Fin)⟶ω
99	98	ffvelrni 6942	. . . . . . . . . . . . . . . 16 ⊢ ({𝑏} ∈ (𝒫 ω ∩ Fin) → (𝐹‘{𝑏}) ∈ ω)
100	60, 99	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘{𝑏}) ∈ ω)
101	98	ffvelrni 6942	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) → (𝐹‘(𝐴 ∩ 𝑏)) ∈ ω)
102	65, 101	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘(𝐴 ∩ 𝑏)) ∈ ω)
103	98	ffvelrni 6942	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∩ 𝑏) ∈ (𝒫 ω ∩ Fin) → (𝐹‘(𝐵 ∩ 𝑏)) ∈ ω)
104	86, 103	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (𝐹‘(𝐵 ∩ 𝑏)) ∈ ω)
105		nnacan 8421	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘{𝑏}) ∈ ω ∧ (𝐹‘(𝐴 ∩ 𝑏)) ∈ ω ∧ (𝐹‘(𝐵 ∩ 𝑏)) ∈ ω) → (((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
106	100, 102, 104, 105	syl3anc 1369	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin))) → (((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
107	106	3adant3 1130	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
108	107	3ad2ant1 1131	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (((𝐹‘{𝑏}) +_o (𝐹‘(𝐴 ∩ 𝑏))) = ((𝐹‘{𝑏}) +_o (𝐹‘(𝐵 ∩ 𝑏))) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
109	97, 108	mpbid 231	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)))
110		uneq2 4087	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → ({𝑏} ∪ (𝐴 ∩ 𝑏)) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
111	110	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → ({𝑏} ∪ (𝐴 ∩ 𝑏)) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
112	56	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = ({𝑏} ∪ (𝐴 ∩ 𝑏)))
113	80	ad2antlr 723	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐵 ∩ suc 𝑏) = ({𝑏} ∪ (𝐵 ∩ 𝑏)))
114	111, 112, 113	3eqtr4d 2788	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))
115	114	ex 412	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
116	115	3adant1 1128	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
117	109, 116	embantd 59	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
118	117	3exp 1117	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ 𝐴 → (𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
119		simp13 1203	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
120	119	eqcomd 2744	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
121		simp12r 1285	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐵 ∈ (𝒫 ω ∩ Fin))
122		simp12l 1284	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐴 ∈ (𝒫 ω ∩ Fin))
123		simp11 1201	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ ω)
124		simp3 1136	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
125		simp2 1135	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ¬ 𝑏 ∈ 𝐴)
126	63	ackbij1lem15 9921	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ (𝒫 ω ∩ Fin) ∧ 𝐴 ∈ (𝒫 ω ∩ Fin)) ∧ (𝑏 ∈ ω ∧ 𝑏 ∈ 𝐵 ∧ ¬ 𝑏 ∈ 𝐴)) → ¬ (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
127	121, 122, 123, 124, 125, 126	syl23anc 1375	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ¬ (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ suc 𝑏)))
128	120, 127	pm2.21dd 194	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
129	128	3exp 1117	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (¬ 𝑏 ∈ 𝐴 → (𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
130	118, 129	pm2.61d 179	. . . . . . . 8 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))))
131		simp13 1203	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
132		simp12l 1284	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝐴 ∈ (𝒫 ω ∩ Fin))
133		simp12r 1285	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝐵 ∈ (𝒫 ω ∩ Fin))
134		simp11 1201	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝑏 ∈ ω)
135		simp2 1135	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐴)
136		simp3 1136	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ¬ 𝑏 ∈ 𝐵)
137	63	ackbij1lem15 9921	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝑏 ∈ ω ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵)) → ¬ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
138	132, 133, 134, 135, 136, 137	syl23anc 1375	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ¬ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
139	131, 138	pm2.21dd 194	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
140	139	3exp 1117	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (𝑏 ∈ 𝐴 → (¬ 𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
141		simp13 1203	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)))
142		ackbij1lem1 9907	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑏 ∈ 𝐴 → (𝐴 ∩ suc 𝑏) = (𝐴 ∩ 𝑏))
143	142	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐴 ∩ suc 𝑏) = (𝐴 ∩ 𝑏))
144	143	fveq2d 6760	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐴 ∩ 𝑏)))
145		ackbij1lem1 9907	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑏 ∈ 𝐵 → (𝐵 ∩ suc 𝑏) = (𝐵 ∩ 𝑏))
146	145	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐵 ∩ suc 𝑏) = (𝐵 ∩ 𝑏))
147	146	fveq2d 6760	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐵 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)))
148	144, 147	eqeq12d 2754	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) ↔ (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
149	148	biimpd 228	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
150	149	3adant1 1128	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏)) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏))))
151	141, 150	mpd 15	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)))
152	143, 146	eqeq12d 2754	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏) ↔ (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)))
153	152	biimprd 247	. . . . . . . . . . . 12 ⊢ ((¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
154	153	3adant1 1128	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → ((𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
155	151, 154	embantd 59	. . . . . . . . . 10 ⊢ (((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
156	155	3exp 1117	. . . . . . . . 9 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (¬ 𝑏 ∈ 𝐴 → (¬ 𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))))
157	140, 156	pm2.61d 179	. . . . . . . 8 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (¬ 𝑏 ∈ 𝐵 → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏))))
158	130, 157	pm2.61d 179	. . . . . . 7 ⊢ ((𝑏 ∈ ω ∧ (𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝐹‘(𝐴 ∩ suc 𝑏)) = (𝐹‘(𝐵 ∩ suc 𝑏))) → (((𝐹‘(𝐴 ∩ 𝑏)) = (𝐹‘(𝐵 ∩ 𝑏)) → (𝐴 ∩ 𝑏) = (𝐵 ∩ 𝑏)) → (𝐴 ∩ suc 𝑏) = (𝐵 ∩ suc 𝑏)))
159	158	3exp 1117	. . . . . 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 7719	. . 3 ⊢ (suc ∪ (𝐴 ∪ 𝐵) ∈ ω → ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)))))
163	17, 162	mpcom 38	. 2 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))))
164		omsson 7691	. . . . . . . 8 ⊢ ω ⊆ On
165	8, 164	sstrdi 3929	. . . . . . 7 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ⊆ On)
166		onsucuni 7650	. . . . . . 7 ⊢ ((𝐴 ∪ 𝐵) ⊆ On → (𝐴 ∪ 𝐵) ⊆ suc ∪ (𝐴 ∪ 𝐵))
167	165, 166	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ⊆ suc ∪ (𝐴 ∪ 𝐵))
168	167	unssad 4117	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐴 ⊆ suc ∪ (𝐴 ∪ 𝐵))
169		df-ss 3900	. . . . 5 ⊢ (𝐴 ⊆ suc ∪ (𝐴 ∪ 𝐵) ↔ (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐴)
170	168, 169	sylib 217	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐴)
171	170	fveq2d 6760	. . 3 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘𝐴))
172	167	unssbd 4118	. . . . 5 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → 𝐵 ⊆ suc ∪ (𝐴 ∪ 𝐵))
173		df-ss 3900	. . . . 5 ⊢ (𝐵 ⊆ suc ∪ (𝐴 ∪ 𝐵) ↔ (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐵)
174	172, 173	sylib 217	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)) = 𝐵)
175	174	fveq2d 6760	. . 3 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘𝐵))
176	171, 175	eqeq12d 2754	. 2 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘(𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵))) = (𝐹‘(𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵))) ↔ (𝐹‘𝐴) = (𝐹‘𝐵)))
177	170, 174	eqeq12d 2754	. 2 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐴 ∩ suc ∪ (𝐴 ∪ 𝐵)) = (𝐵 ∩ suc ∪ (𝐴 ∪ 𝐵)) ↔ 𝐴 = 𝐵))
178	163, 176, 177	3imtr3d 292	1 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘𝐴) = (𝐹‘𝐵) → 𝐴 = 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 ∅c0 4253 𝒫 cpw 4530 {csn 4558 ∪ cuni 4836 ∪ ciun 4921 ↦ cmpt 5153 × cxp 5578 Ord word 6250 Oncon0 6251 suc csuc 6253 ‘cfv 6418 (class class class)co 7255 ωcom 7687 +_o coa 8264 Fincfn 8691 cardccrd 9624

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-reu 3070 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-2o 8268 df-oadd 8271 df-er 8456 df-map 8575 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-dju 9590 df-card 9628

This theorem is referenced by: ackbij1lem17 9923

W3C validator