Theorem onfr 6374

Description: The ordinal class is well-founded. This proof does not require the axiom of regularity. This lemma is used in ordon 7756 (through epweon 7754) in order to eliminate the need for the axiom of regularity. (Contributed by NM, 17-May-1994.)

Assertion

Ref	Expression
onfr	⊢ E Fr On

Proof of Theorem onfr

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfepfr 5625	. 2 ⊢ ( E Fr On ↔ ∀𝑥((𝑥 ⊆ On ∧ 𝑥 ≠ ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅))
2		n0 4319	. . . 4 ⊢ (𝑥 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝑥)
3		ineq2 4180	. . . . . . . . . 10 ⊢ (𝑧 = 𝑦 → (𝑥 ∩ 𝑧) = (𝑥 ∩ 𝑦))
4	3	eqeq1d 2732	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → ((𝑥 ∩ 𝑧) = ∅ ↔ (𝑥 ∩ 𝑦) = ∅))
5	4	rspcev 3591	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝑥 ∩ 𝑦) = ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)
6	5	adantll 714	. . . . . . 7 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) = ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)
7		inss1 4203	. . . . . . . 8 ⊢ (𝑥 ∩ 𝑦) ⊆ 𝑥
8		ssel2 3944	. . . . . . . . . . 11 ⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
9		eloni 6345	. . . . . . . . . . 11 ⊢ (𝑦 ∈ On → Ord 𝑦)
10		ordfr 6350	. . . . . . . . . . 11 ⊢ (Ord 𝑦 → E Fr 𝑦)
11	8, 9, 10	3syl 18	. . . . . . . . . 10 ⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → E Fr 𝑦)
12		inss2 4204	. . . . . . . . . . 11 ⊢ (𝑥 ∩ 𝑦) ⊆ 𝑦
13		vex 3454	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
14	13	inex1 5275	. . . . . . . . . . . 12 ⊢ (𝑥 ∩ 𝑦) ∈ V
15	14	epfrc 5626	. . . . . . . . . . 11 ⊢ (( E Fr 𝑦 ∧ (𝑥 ∩ 𝑦) ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅)
16	12, 15	mp3an2 1451	. . . . . . . . . 10 ⊢ (( E Fr 𝑦 ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅)
17	11, 16	sylan 580	. . . . . . . . 9 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅)
18		inass 4194	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ 𝑦) ∩ 𝑧) = (𝑥 ∩ (𝑦 ∩ 𝑧))
19	8, 9	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → Ord 𝑦)
20		elinel2 4168	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (𝑥 ∩ 𝑦) → 𝑧 ∈ 𝑦)
21		ordelss 6351	. . . . . . . . . . . . . . . 16 ⊢ ((Ord 𝑦 ∧ 𝑧 ∈ 𝑦) → 𝑧 ⊆ 𝑦)
22	19, 20, 21	syl2an 596	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → 𝑧 ⊆ 𝑦)
23		sseqin2 4189	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ⊆ 𝑦 ↔ (𝑦 ∩ 𝑧) = 𝑧)
24	22, 23	sylib 218	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → (𝑦 ∩ 𝑧) = 𝑧)
25	24	ineq2d 4186	. . . . . . . . . . . . 13 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → (𝑥 ∩ (𝑦 ∩ 𝑧)) = (𝑥 ∩ 𝑧))
26	18, 25	eqtrid 2777	. . . . . . . . . . . 12 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → ((𝑥 ∩ 𝑦) ∩ 𝑧) = (𝑥 ∩ 𝑧))
27	26	eqeq1d 2732	. . . . . . . . . . 11 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → (((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅ ↔ (𝑥 ∩ 𝑧) = ∅))
28	27	rexbidva 3156	. . . . . . . . . 10 ⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → (∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅ ↔ ∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅))
29	28	adantr 480	. . . . . . . . 9 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → (∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅ ↔ ∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅))
30	17, 29	mpbid 232	. . . . . . . 8 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅)
31		ssrexv 4019	. . . . . . . 8 ⊢ ((𝑥 ∩ 𝑦) ⊆ 𝑥 → (∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅ → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅))
32	7, 30, 31	mpsyl 68	. . . . . . 7 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)
33	6, 32	pm2.61dane 3013	. . . . . 6 ⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)
34	33	ex 412	. . . . 5 ⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅))
35	34	exlimdv 1933	. . . 4 ⊢ (𝑥 ⊆ On → (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅))
36	2, 35	biimtrid 242	. . 3 ⊢ (𝑥 ⊆ On → (𝑥 ≠ ∅ → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅))
37	36	imp 406	. 2 ⊢ ((𝑥 ⊆ On ∧ 𝑥 ≠ ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)
38	1, 37	mpgbir 1799	1 ⊢ E Fr On

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2926  ∃wrex 3054   ∩ cin 3916   ⊆ wss 3917  ∅c0 4299   E cep 5540   Fr wfr 5591  Ord word 6334  Oncon0 6335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-tr 5218  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-on 6339

This theorem is referenced by:  epweon  7754  epweonALT  7755  on2recsfn  8634  on2recsov  8635  on2ind  8636  on3ind  8637  wffr  44958