Theorem onfr 6434

Description: The ordinal class is well-founded. This proof does not require the axiom of regularity. This lemma is used in ordon 7812 (through epweon 7810) 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 5684	. 2 ⊢ ( E Fr On ↔ ∀𝑥((𝑥 ⊆ On ∧ 𝑥 ≠ ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅))
2		n0 4376	. . . 4 ⊢ (𝑥 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝑥)
3		ineq2 4235	. . . . . . . . . 10 ⊢ (𝑧 = 𝑦 → (𝑥 ∩ 𝑧) = (𝑥 ∩ 𝑦))
4	3	eqeq1d 2742	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → ((𝑥 ∩ 𝑧) = ∅ ↔ (𝑥 ∩ 𝑦) = ∅))
5	4	rspcev 3635	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝑥 ∩ 𝑦) = ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)
6	5	adantll 713	. . . . . . 7 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) = ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)
7		inss1 4258	. . . . . . . 8 ⊢ (𝑥 ∩ 𝑦) ⊆ 𝑥
8		ssel2 4003	. . . . . . . . . . 11 ⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
9		eloni 6405	. . . . . . . . . . 11 ⊢ (𝑦 ∈ On → Ord 𝑦)
10		ordfr 6410	. . . . . . . . . . 11 ⊢ (Ord 𝑦 → E Fr 𝑦)
11	8, 9, 10	3syl 18	. . . . . . . . . 10 ⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → E Fr 𝑦)
12		inss2 4259	. . . . . . . . . . 11 ⊢ (𝑥 ∩ 𝑦) ⊆ 𝑦
13		vex 3492	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
14	13	inex1 5335	. . . . . . . . . . . 12 ⊢ (𝑥 ∩ 𝑦) ∈ V
15	14	epfrc 5685	. . . . . . . . . . 11 ⊢ (( E Fr 𝑦 ∧ (𝑥 ∩ 𝑦) ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅)
16	12, 15	mp3an2 1449	. . . . . . . . . 10 ⊢ (( E Fr 𝑦 ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅)
17	11, 16	sylan 579	. . . . . . . . 9 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅)
18		inass 4249	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ 𝑦) ∩ 𝑧) = (𝑥 ∩ (𝑦 ∩ 𝑧))
19	8, 9	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → Ord 𝑦)
20		elinel2 4225	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (𝑥 ∩ 𝑦) → 𝑧 ∈ 𝑦)
21		ordelss 6411	. . . . . . . . . . . . . . . 16 ⊢ ((Ord 𝑦 ∧ 𝑧 ∈ 𝑦) → 𝑧 ⊆ 𝑦)
22	19, 20, 21	syl2an 595	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → 𝑧 ⊆ 𝑦)
23		sseqin2 4244	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ⊆ 𝑦 ↔ (𝑦 ∩ 𝑧) = 𝑧)
24	22, 23	sylib 218	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → (𝑦 ∩ 𝑧) = 𝑧)
25	24	ineq2d 4241	. . . . . . . . . . . . 13 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → (𝑥 ∩ (𝑦 ∩ 𝑧)) = (𝑥 ∩ 𝑧))
26	18, 25	eqtrid 2792	. . . . . . . . . . . 12 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → ((𝑥 ∩ 𝑦) ∩ 𝑧) = (𝑥 ∩ 𝑧))
27	26	eqeq1d 2742	. . . . . . . . . . 11 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → (((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅ ↔ (𝑥 ∩ 𝑧) = ∅))
28	27	rexbidva 3183	. . . . . . . . . 10 ⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → (∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅ ↔ ∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅))
29	28	adantr 480	. . . . . . . . 9 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → (∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅ ↔ ∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅))
30	17, 29	mpbid 232	. . . . . . . 8 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅)
31		ssrexv 4078	. . . . . . . 8 ⊢ ((𝑥 ∩ 𝑦) ⊆ 𝑥 → (∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅ → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅))
32	7, 30, 31	mpsyl 68	. . . . . . 7 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)
33	6, 32	pm2.61dane 3035	. . . . . 6 ⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)
34	33	ex 412	. . . . 5 ⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅))
35	34	exlimdv 1932	. . . 4 ⊢ (𝑥 ⊆ On → (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅))
36	2, 35	biimtrid 242	. . 3 ⊢ (𝑥 ⊆ On → (𝑥 ≠ ∅ → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅))
37	36	imp 406	. 2 ⊢ ((𝑥 ⊆ On ∧ 𝑥 ≠ ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)
38	1, 37	mpgbir 1797	1 ⊢ E Fr On

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537  ∃wex 1777   ∈ wcel 2108   ≠ wne 2946  ∃wrex 3076   ∩ cin 3975   ⊆ wss 3976  ∅c0 4352   E cep 5598   Fr wfr 5649  Ord word 6394  Oncon0 6395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-tr 5284  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-ord 6398  df-on 6399

This theorem is referenced by:  epweon  7810  epweonALT  7811  on2recsfn  8723  on2recsov  8724  on2ind  8725  on3ind  8726