Theorem ac10ct 10057

Description: A proof of the well-ordering theorem weth 10518, an Axiom of Choice equivalent, restricted to sets dominated by some ordinal (in particular finite sets and countable sets), proven in ZF without AC. (Contributed by Mario Carneiro, 5-Jan-2013.)

Assertion

Ref	Expression
ac10ct	⊢ (∃𝑦 ∈ On 𝐴 ≼ 𝑦 → ∃𝑥 𝑥 We 𝐴)

Distinct variable group:   𝑥,𝐴,𝑦

Proof of Theorem ac10ct

Dummy variables 𝑓 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3468	. . . . . 6 ⊢ 𝑦 ∈ V
2	1	brdom 8984	. . . . 5 ⊢ (𝐴 ≼ 𝑦 ↔ ∃𝑓 𝑓:𝐴–1-1→𝑦)
3		f1f 6785	. . . . . . . . . . . 12 ⊢ (𝑓:𝐴–1-1→𝑦 → 𝑓:𝐴⟶𝑦)
4	3	frnd 6725	. . . . . . . . . . 11 ⊢ (𝑓:𝐴–1-1→𝑦 → ran 𝑓 ⊆ 𝑦)
5		onss 7788	. . . . . . . . . . 11 ⊢ (𝑦 ∈ On → 𝑦 ⊆ On)
6		sstr2 3972	. . . . . . . . . . 11 ⊢ (ran 𝑓 ⊆ 𝑦 → (𝑦 ⊆ On → ran 𝑓 ⊆ On))
7	4, 5, 6	syl2im 40	. . . . . . . . . 10 ⊢ (𝑓:𝐴–1-1→𝑦 → (𝑦 ∈ On → ran 𝑓 ⊆ On))
8		epweon 7778	. . . . . . . . . 10 ⊢ E We On
9		wess 5653	. . . . . . . . . 10 ⊢ (ran 𝑓 ⊆ On → ( E We On → E We ran 𝑓))
10	7, 8, 9	syl6mpi 67	. . . . . . . . 9 ⊢ (𝑓:𝐴–1-1→𝑦 → (𝑦 ∈ On → E We ran 𝑓))
11	10	adantl 481	. . . . . . . 8 ⊢ ((𝐴 ≼ 𝑦 ∧ 𝑓:𝐴–1-1→𝑦) → (𝑦 ∈ On → E We ran 𝑓))
12		f1f1orn 6840	. . . . . . . . . 10 ⊢ (𝑓:𝐴–1-1→𝑦 → 𝑓:𝐴–1-1-onto→ran 𝑓)
13		eqid 2734	. . . . . . . . . . 11 ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} = {⟨𝑤, 𝑧⟩ ∣ (𝑓‘𝑤) E (𝑓‘𝑧)}
14	13	f1owe 7356	. . . . . . . . . 10 ⊢ (𝑓:𝐴–1-1-onto→ran 𝑓 → ( E We ran 𝑓 → {⟨𝑤, 𝑧⟩ ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} We 𝐴))
15	12, 14	syl 17	. . . . . . . . 9 ⊢ (𝑓:𝐴–1-1→𝑦 → ( E We ran 𝑓 → {⟨𝑤, 𝑧⟩ ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} We 𝐴))
16		weinxp 5752	. . . . . . . . . 10 ⊢ ({⟨𝑤, 𝑧⟩ ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} We 𝐴 ↔ ({⟨𝑤, 𝑧⟩ ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) We 𝐴)
17		reldom 8974	. . . . . . . . . . . 12 ⊢ Rel ≼
18	17	brrelex1i 5723	. . . . . . . . . . 11 ⊢ (𝐴 ≼ 𝑦 → 𝐴 ∈ V)
19		sqxpexg 7758	. . . . . . . . . . 11 ⊢ (𝐴 ∈ V → (𝐴 × 𝐴) ∈ V)
20		incom 4191	. . . . . . . . . . . 12 ⊢ ((𝐴 × 𝐴) ∩ {⟨𝑤, 𝑧⟩ ∣ (𝑓‘𝑤) E (𝑓‘𝑧)}) = ({⟨𝑤, 𝑧⟩ ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴))
21		inex1g 5301	. . . . . . . . . . . 12 ⊢ ((𝐴 × 𝐴) ∈ V → ((𝐴 × 𝐴) ∩ {⟨𝑤, 𝑧⟩ ∣ (𝑓‘𝑤) E (𝑓‘𝑧)}) ∈ V)
22	20, 21	eqeltrrid 2838	. . . . . . . . . . 11 ⊢ ((𝐴 × 𝐴) ∈ V → ({⟨𝑤, 𝑧⟩ ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) ∈ V)
23		weeq1 5654	. . . . . . . . . . . 12 ⊢ (𝑥 = ({⟨𝑤, 𝑧⟩ ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) → (𝑥 We 𝐴 ↔ ({⟨𝑤, 𝑧⟩ ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) We 𝐴))
24	23	spcegv 3581	. . . . . . . . . . 11 ⊢ (({⟨𝑤, 𝑧⟩ ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) ∈ V → (({⟨𝑤, 𝑧⟩ ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑥 𝑥 We 𝐴))
25	18, 19, 22, 24	4syl 19	. . . . . . . . . 10 ⊢ (𝐴 ≼ 𝑦 → (({⟨𝑤, 𝑧⟩ ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑥 𝑥 We 𝐴))
26	16, 25	biimtrid 242	. . . . . . . . 9 ⊢ (𝐴 ≼ 𝑦 → ({⟨𝑤, 𝑧⟩ ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} We 𝐴 → ∃𝑥 𝑥 We 𝐴))
27	15, 26	sylan9r 508	. . . . . . . 8 ⊢ ((𝐴 ≼ 𝑦 ∧ 𝑓:𝐴–1-1→𝑦) → ( E We ran 𝑓 → ∃𝑥 𝑥 We 𝐴))
28	11, 27	syld 47	. . . . . . 7 ⊢ ((𝐴 ≼ 𝑦 ∧ 𝑓:𝐴–1-1→𝑦) → (𝑦 ∈ On → ∃𝑥 𝑥 We 𝐴))
29	28	impancom 451	. . . . . 6 ⊢ ((𝐴 ≼ 𝑦 ∧ 𝑦 ∈ On) → (𝑓:𝐴–1-1→𝑦 → ∃𝑥 𝑥 We 𝐴))
30	29	exlimdv 1932	. . . . 5 ⊢ ((𝐴 ≼ 𝑦 ∧ 𝑦 ∈ On) → (∃𝑓 𝑓:𝐴–1-1→𝑦 → ∃𝑥 𝑥 We 𝐴))
31	2, 30	biimtrid 242	. . . 4 ⊢ ((𝐴 ≼ 𝑦 ∧ 𝑦 ∈ On) → (𝐴 ≼ 𝑦 → ∃𝑥 𝑥 We 𝐴))
32	31	ex 412	. . 3 ⊢ (𝐴 ≼ 𝑦 → (𝑦 ∈ On → (𝐴 ≼ 𝑦 → ∃𝑥 𝑥 We 𝐴)))
33	32	pm2.43b 55	. 2 ⊢ (𝑦 ∈ On → (𝐴 ≼ 𝑦 → ∃𝑥 𝑥 We 𝐴))
34	33	rexlimiv 3135	1 ⊢ (∃𝑦 ∈ On 𝐴 ≼ 𝑦 → ∃𝑥 𝑥 We 𝐴)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1778   ∈ wcel 2107  ∃wrex 3059  Vcvv 3464   ∩ cin 3932   ⊆ wss 3933   class class class wbr 5125  {copab 5187   E cep 5565   We wwe 5618   × cxp 5665  ran crn 5668  Oncon0 6365  –1-1→wf1 6539  –1-1-onto→wf1o 6541  ‘cfv 6542   ≼ cdom 8966

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5261  ax-sep 5278  ax-nul 5288  ax-pow 5347  ax-pr 5414  ax-un 7738

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3421  df-v 3466  df-dif 3936  df-un 3938  df-in 3940  df-ss 3950  df-pss 3953  df-nul 4316  df-if 4508  df-pw 4584  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-br 5126  df-opab 5188  df-tr 5242  df-id 5560  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-ord 6368  df-on 6369  df-iota 6495  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-dom 8970

This theorem is referenced by:  ondomen  10060