Theorem onint 7735

Description: The intersection (infimum) of a nonempty class of ordinal numbers belongs to the class. Compare Exercise 4 of [TakeutiZaring] p. 45. (Contributed by NM, 31-Jan-1997.)

Assertion

Ref	Expression
onint	⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝐴)

Proof of Theorem onint

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

Step	Hyp	Ref	Expression
1		ordon 7722	. . . 4 ⊢ Ord On
2		tz7.5 6336	. . . 4 ⊢ ((Ord On ∧ 𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (𝐴 ∩ 𝑥) = ∅)
3	1, 2	mp3an1 1451	. . 3 ⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (𝐴 ∩ 𝑥) = ∅)
4		ssel 3916	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → 𝑥 ∈ On))
5	4	imdistani 568	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴) → (𝐴 ⊆ On ∧ 𝑥 ∈ On))
6		ssel 3916	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ⊆ On → (𝑧 ∈ 𝐴 → 𝑧 ∈ On))
7		ontri1 6349	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (𝑥 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑥))
8		ssel 3916	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ⊆ 𝑧 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧))
9	7, 8	biimtrrdi 254	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (¬ 𝑧 ∈ 𝑥 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧)))
10	9	ex 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ On → (𝑧 ∈ On → (¬ 𝑧 ∈ 𝑥 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧))))
11	6, 10	sylan9 507	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ⊆ On ∧ 𝑥 ∈ On) → (𝑧 ∈ 𝐴 → (¬ 𝑧 ∈ 𝑥 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧))))
12	11	com4r 94	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝑥 → ((𝐴 ⊆ On ∧ 𝑥 ∈ On) → (𝑧 ∈ 𝐴 → (¬ 𝑧 ∈ 𝑥 → 𝑦 ∈ 𝑧))))
13	12	imp31 417	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ 𝑥 ∧ (𝐴 ⊆ On ∧ 𝑥 ∈ On)) ∧ 𝑧 ∈ 𝐴) → (¬ 𝑧 ∈ 𝑥 → 𝑦 ∈ 𝑧))
14	13	ralimdva 3150	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝐴 ⊆ On ∧ 𝑥 ∈ On)) → (∀𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑥 → ∀𝑧 ∈ 𝐴 𝑦 ∈ 𝑧))
15		disj 4391	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∩ 𝑥) = ∅ ↔ ∀𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑥)
16		vex 3434	. . . . . . . . . . . . . . . . 17 ⊢ 𝑦 ∈ V
17	16	elint2 4897	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ∩ 𝐴 ↔ ∀𝑧 ∈ 𝐴 𝑦 ∈ 𝑧)
18	14, 15, 17	3imtr4g 296	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝐴 ⊆ On ∧ 𝑥 ∈ On)) → ((𝐴 ∩ 𝑥) = ∅ → 𝑦 ∈ ∩ 𝐴))
19	5, 18	sylan2 594	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴)) → ((𝐴 ∩ 𝑥) = ∅ → 𝑦 ∈ ∩ 𝐴))
20	19	exp32 420	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝑥 → (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → ((𝐴 ∩ 𝑥) = ∅ → 𝑦 ∈ ∩ 𝐴))))
21	20	com4l 92	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → ((𝐴 ∩ 𝑥) = ∅ → (𝑦 ∈ 𝑥 → 𝑦 ∈ ∩ 𝐴))))
22	21	imp32 418	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ (𝐴 ∩ 𝑥) = ∅)) → (𝑦 ∈ 𝑥 → 𝑦 ∈ ∩ 𝐴))
23	22	ssrdv 3928	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ (𝐴 ∩ 𝑥) = ∅)) → 𝑥 ⊆ ∩ 𝐴)
24		intss1 4906	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
25	24	ad2antrl 729	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ (𝐴 ∩ 𝑥) = ∅)) → ∩ 𝐴 ⊆ 𝑥)
26	23, 25	eqssd 3940	. . . . . . . . 9 ⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ (𝐴 ∩ 𝑥) = ∅)) → 𝑥 = ∩ 𝐴)
27	26	eleq1d 2822	. . . . . . . 8 ⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ (𝐴 ∩ 𝑥) = ∅)) → (𝑥 ∈ 𝐴 ↔ ∩ 𝐴 ∈ 𝐴))
28	27	biimpd 229	. . . . . . 7 ⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ (𝐴 ∩ 𝑥) = ∅)) → (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ 𝐴))
29	28	exp32 420	. . . . . 6 ⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → ((𝐴 ∩ 𝑥) = ∅ → (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ 𝐴))))
30	29	com34 91	. . . . 5 ⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → ((𝐴 ∩ 𝑥) = ∅ → ∩ 𝐴 ∈ 𝐴))))
31	30	pm2.43d 53	. . . 4 ⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → ((𝐴 ∩ 𝑥) = ∅ → ∩ 𝐴 ∈ 𝐴)))
32	31	rexlimdv 3137	. . 3 ⊢ (𝐴 ⊆ On → (∃𝑥 ∈ 𝐴 (𝐴 ∩ 𝑥) = ∅ → ∩ 𝐴 ∈ 𝐴))
33	3, 32	syl5 34	. 2 ⊢ (𝐴 ⊆ On → ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝐴))
34	33	anabsi5 670	1 ⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062   ∩ cin 3889   ⊆ wss 3890  ∅c0 4274  ∩ cint 4890  Ord word 6314  Oncon0 6315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-ord 6318  df-on 6319

This theorem is referenced by:  onint0  7736  onssmin  7737  onminesb  7738  onminsb  7739  oninton  7740  oneqmin  7745  oeeulem  8528  nnawordex  8564  unblem1  9193  unblem2  9194  tz9.12lem3  9702  scott0  9799  cardid2  9866  ackbij1lem18  10147  cardcf  10163  cff1  10169  cflim2  10174  cfss  10176  cofsmo  10180  fin23lem26  10236  pwfseqlem3  10572  gruina  10730  2ndcdisj  23430  ltsval2  27639  nobdaymin  27764  lrrecfr  27954  rankeq1o  36374  regsfromunir1  36743  dnnumch3  43490  oninfint  43679  inaex  44739