Theorem unfilem1 8473

Description: Lemma for proving that the union of two finite sets is finite. (Contributed by NM, 10-Nov-2002.) (Revised by Mario Carneiro, 31-Aug-2015.)

Hypotheses

Ref	Expression
unfilem1.1	⊢ 𝐴 ∈ ω
unfilem1.2	⊢ 𝐵 ∈ ω
unfilem1.3	⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))

Assertion

Ref	Expression
unfilem1	⊢ ran 𝐹 = ((𝐴 +𝑜 𝐵) ∖ 𝐴)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝐹(𝑥)

Proof of Theorem unfilem1

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		unfilem1.2	. . . . . . . . . 10 ⊢ 𝐵 ∈ ω
2		elnn 7315	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝑥 ∈ ω)
3	1, 2	mpan2 674	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐵 → 𝑥 ∈ ω)
4		unfilem1.1	. . . . . . . . . 10 ⊢ 𝐴 ∈ ω
5		nnaord 7946	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ∈ ω) → (𝑥 ∈ 𝐵 ↔ (𝐴 +𝑜 𝑥) ∈ (𝐴 +𝑜 𝐵)))
6	1, 4, 5	mp3an23 1570	. . . . . . . . 9 ⊢ (𝑥 ∈ ω → (𝑥 ∈ 𝐵 ↔ (𝐴 +𝑜 𝑥) ∈ (𝐴 +𝑜 𝐵)))
7	3, 6	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐵 ↔ (𝐴 +𝑜 𝑥) ∈ (𝐴 +𝑜 𝐵)))
8	7	ibi 258	. . . . . . 7 ⊢ (𝑥 ∈ 𝐵 → (𝐴 +𝑜 𝑥) ∈ (𝐴 +𝑜 𝐵))
9		nnaword1 7956	. . . . . . . . 9 ⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → 𝐴 ⊆ (𝐴 +𝑜 𝑥))
10		nnord 7313	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ω → Ord 𝐴)
11	4, 10	ax-mp 5	. . . . . . . . . 10 ⊢ Ord 𝐴
12		nnacl 7938	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 +𝑜 𝑥) ∈ ω)
13		nnord 7313	. . . . . . . . . . 11 ⊢ ((𝐴 +𝑜 𝑥) ∈ ω → Ord (𝐴 +𝑜 𝑥))
14	12, 13	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → Ord (𝐴 +𝑜 𝑥))
15		ordtri1 5983	. . . . . . . . . 10 ⊢ ((Ord 𝐴 ∧ Ord (𝐴 +𝑜 𝑥)) → (𝐴 ⊆ (𝐴 +𝑜 𝑥) ↔ ¬ (𝐴 +𝑜 𝑥) ∈ 𝐴))
16	11, 14, 15	sylancr 577	. . . . . . . . 9 ⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 ⊆ (𝐴 +𝑜 𝑥) ↔ ¬ (𝐴 +𝑜 𝑥) ∈ 𝐴))
17	9, 16	mpbid 223	. . . . . . . 8 ⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → ¬ (𝐴 +𝑜 𝑥) ∈ 𝐴)
18	4, 3, 17	sylancr 577	. . . . . . 7 ⊢ (𝑥 ∈ 𝐵 → ¬ (𝐴 +𝑜 𝑥) ∈ 𝐴)
19	8, 18	jca 503	. . . . . 6 ⊢ (𝑥 ∈ 𝐵 → ((𝐴 +𝑜 𝑥) ∈ (𝐴 +𝑜 𝐵) ∧ ¬ (𝐴 +𝑜 𝑥) ∈ 𝐴))
20		eleq1 2884	. . . . . . . 8 ⊢ (𝑦 = (𝐴 +𝑜 𝑥) → (𝑦 ∈ (𝐴 +𝑜 𝐵) ↔ (𝐴 +𝑜 𝑥) ∈ (𝐴 +𝑜 𝐵)))
21		eleq1 2884	. . . . . . . . 9 ⊢ (𝑦 = (𝐴 +𝑜 𝑥) → (𝑦 ∈ 𝐴 ↔ (𝐴 +𝑜 𝑥) ∈ 𝐴))
22	21	notbid 309	. . . . . . . 8 ⊢ (𝑦 = (𝐴 +𝑜 𝑥) → (¬ 𝑦 ∈ 𝐴 ↔ ¬ (𝐴 +𝑜 𝑥) ∈ 𝐴))
23	20, 22	anbi12d 618	. . . . . . 7 ⊢ (𝑦 = (𝐴 +𝑜 𝑥) → ((𝑦 ∈ (𝐴 +𝑜 𝐵) ∧ ¬ 𝑦 ∈ 𝐴) ↔ ((𝐴 +𝑜 𝑥) ∈ (𝐴 +𝑜 𝐵) ∧ ¬ (𝐴 +𝑜 𝑥) ∈ 𝐴)))
24	23	biimparc 467	. . . . . 6 ⊢ ((((𝐴 +𝑜 𝑥) ∈ (𝐴 +𝑜 𝐵) ∧ ¬ (𝐴 +𝑜 𝑥) ∈ 𝐴) ∧ 𝑦 = (𝐴 +𝑜 𝑥)) → (𝑦 ∈ (𝐴 +𝑜 𝐵) ∧ ¬ 𝑦 ∈ 𝐴))
25	19, 24	sylan 571	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 = (𝐴 +𝑜 𝑥)) → (𝑦 ∈ (𝐴 +𝑜 𝐵) ∧ ¬ 𝑦 ∈ 𝐴))
26	25	rexlimiva 3227	. . . 4 ⊢ (∃𝑥 ∈ 𝐵 𝑦 = (𝐴 +𝑜 𝑥) → (𝑦 ∈ (𝐴 +𝑜 𝐵) ∧ ¬ 𝑦 ∈ 𝐴))
27	4, 1	nnacli 7941	. . . . . . . 8 ⊢ (𝐴 +𝑜 𝐵) ∈ ω
28		elnn 7315	. . . . . . . 8 ⊢ ((𝑦 ∈ (𝐴 +𝑜 𝐵) ∧ (𝐴 +𝑜 𝐵) ∈ ω) → 𝑦 ∈ ω)
29	27, 28	mpan2 674	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 +𝑜 𝐵) → 𝑦 ∈ ω)
30		nnord 7313	. . . . . . . . 9 ⊢ (𝑦 ∈ ω → Ord 𝑦)
31		ordtri1 5983	. . . . . . . . 9 ⊢ ((Ord 𝐴 ∧ Ord 𝑦) → (𝐴 ⊆ 𝑦 ↔ ¬ 𝑦 ∈ 𝐴))
32	10, 30, 31	syl2an 585	. . . . . . . 8 ⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ⊆ 𝑦 ↔ ¬ 𝑦 ∈ 𝐴))
33		nnawordex 7964	. . . . . . . 8 ⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ⊆ 𝑦 ↔ ∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝑦))
34	32, 33	bitr3d 272	. . . . . . 7 ⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (¬ 𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝑦))
35	4, 29, 34	sylancr 577	. . . . . 6 ⊢ (𝑦 ∈ (𝐴 +𝑜 𝐵) → (¬ 𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝑦))
36		eleq1 2884	. . . . . . . . . 10 ⊢ ((𝐴 +𝑜 𝑥) = 𝑦 → ((𝐴 +𝑜 𝑥) ∈ (𝐴 +𝑜 𝐵) ↔ 𝑦 ∈ (𝐴 +𝑜 𝐵)))
37	6, 36	sylan9bb 501	. . . . . . . . 9 ⊢ ((𝑥 ∈ ω ∧ (𝐴 +𝑜 𝑥) = 𝑦) → (𝑥 ∈ 𝐵 ↔ 𝑦 ∈ (𝐴 +𝑜 𝐵)))
38	37	biimprcd 241	. . . . . . . 8 ⊢ (𝑦 ∈ (𝐴 +𝑜 𝐵) → ((𝑥 ∈ ω ∧ (𝐴 +𝑜 𝑥) = 𝑦) → 𝑥 ∈ 𝐵))
39		eqcom 2824	. . . . . . . . . . 11 ⊢ ((𝐴 +𝑜 𝑥) = 𝑦 ↔ 𝑦 = (𝐴 +𝑜 𝑥))
40	39	biimpi 207	. . . . . . . . . 10 ⊢ ((𝐴 +𝑜 𝑥) = 𝑦 → 𝑦 = (𝐴 +𝑜 𝑥))
41	40	adantl 469	. . . . . . . . 9 ⊢ ((𝑥 ∈ ω ∧ (𝐴 +𝑜 𝑥) = 𝑦) → 𝑦 = (𝐴 +𝑜 𝑥))
42	41	a1i 11	. . . . . . . 8 ⊢ (𝑦 ∈ (𝐴 +𝑜 𝐵) → ((𝑥 ∈ ω ∧ (𝐴 +𝑜 𝑥) = 𝑦) → 𝑦 = (𝐴 +𝑜 𝑥)))
43	38, 42	jcad 504	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 +𝑜 𝐵) → ((𝑥 ∈ ω ∧ (𝐴 +𝑜 𝑥) = 𝑦) → (𝑥 ∈ 𝐵 ∧ 𝑦 = (𝐴 +𝑜 𝑥))))
44	43	reximdv2 3212	. . . . . 6 ⊢ (𝑦 ∈ (𝐴 +𝑜 𝐵) → (∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝑦 → ∃𝑥 ∈ 𝐵 𝑦 = (𝐴 +𝑜 𝑥)))
45	35, 44	sylbid 231	. . . . 5 ⊢ (𝑦 ∈ (𝐴 +𝑜 𝐵) → (¬ 𝑦 ∈ 𝐴 → ∃𝑥 ∈ 𝐵 𝑦 = (𝐴 +𝑜 𝑥)))
46	45	imp 395	. . . 4 ⊢ ((𝑦 ∈ (𝐴 +𝑜 𝐵) ∧ ¬ 𝑦 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 𝑦 = (𝐴 +𝑜 𝑥))
47	26, 46	impbii 200	. . 3 ⊢ (∃𝑥 ∈ 𝐵 𝑦 = (𝐴 +𝑜 𝑥) ↔ (𝑦 ∈ (𝐴 +𝑜 𝐵) ∧ ¬ 𝑦 ∈ 𝐴))
48		unfilem1.3	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))
49		ovex 6916	. . . 4 ⊢ (𝐴 +𝑜 𝑥) ∈ V
50	48, 49	elrnmpti 5591	. . 3 ⊢ (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐵 𝑦 = (𝐴 +𝑜 𝑥))
51		eldif 3790	. . 3 ⊢ (𝑦 ∈ ((𝐴 +𝑜 𝐵) ∖ 𝐴) ↔ (𝑦 ∈ (𝐴 +𝑜 𝐵) ∧ ¬ 𝑦 ∈ 𝐴))
52	47, 50, 51	3bitr4i 294	. 2 ⊢ (𝑦 ∈ ran 𝐹 ↔ 𝑦 ∈ ((𝐴 +𝑜 𝐵) ∖ 𝐴))
53	52	eqriv 2814	1 ⊢ ran 𝐹 = ((𝐴 +𝑜 𝐵) ∖ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 197   ∧ wa 384   = wceq 1637   ∈ wcel 2157  ∃wrex 3108   ∖ cdif 3777   ⊆ wss 3780   ↦ cmpt 4934  ran crn 5325  Ord word 5949  (class class class)co 6884  ωcom 7305   +_𝑜 coa 7803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-ord 5953  df-on 5954  df-lim 5955  df-suc 5956  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-ov 6887  df-oprab 6888  df-mpt2 6889  df-om 7306  df-wrecs 7652  df-recs 7714  df-rdg 7752  df-oadd 7810

This theorem is referenced by:  unfilem2  8474