Theorem onint 7718

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 7705	. . . 4 ⊢ Ord On
2		tz7.5 6323	. . . 4 ⊢ ((Ord On ∧ 𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (𝐴 ∩ 𝑥) = ∅)
3	1, 2	mp3an1 1450	. . 3 ⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (𝐴 ∩ 𝑥) = ∅)
4		ssel 3926	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → 𝑥 ∈ On))
5	4	imdistani 568	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴) → (𝐴 ⊆ On ∧ 𝑥 ∈ On))
6		ssel 3926	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ⊆ On → (𝑧 ∈ 𝐴 → 𝑧 ∈ On))
7		ontri1 6336	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (𝑥 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑥))
8		ssel 3926	. . . . . . . . . . . . . . . . . . . . . 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 3142	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝐴 ⊆ On ∧ 𝑥 ∈ On)) → (∀𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑥 → ∀𝑧 ∈ 𝐴 𝑦 ∈ 𝑧))
15		disj 4398	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∩ 𝑥) = ∅ ↔ ∀𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑥)
16		vex 3438	. . . . . . . . . . . . . . . . 17 ⊢ 𝑦 ∈ V
17	16	elint2 4902	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ∩ 𝐴 ↔ ∀𝑧 ∈ 𝐴 𝑦 ∈ 𝑧)
18	14, 15, 17	3imtr4g 296	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝐴 ⊆ On ∧ 𝑥 ∈ On)) → ((𝐴 ∩ 𝑥) = ∅ → 𝑦 ∈ ∩ 𝐴))
19	5, 18	sylan2 593	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴)) → ((𝐴 ∩ 𝑥) = ∅ → 𝑦 ∈ ∩ 𝐴))
20	19	exp32 420	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝑥 → (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → ((𝐴 ∩ 𝑥) = ∅ → 𝑦 ∈ ∩ 𝐴))))
21	20	com4l 92	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → ((𝐴 ∩ 𝑥) = ∅ → (𝑦 ∈ 𝑥 → 𝑦 ∈ ∩ 𝐴))))
22	21	imp32 418	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ (𝐴 ∩ 𝑥) = ∅)) → (𝑦 ∈ 𝑥 → 𝑦 ∈ ∩ 𝐴))
23	22	ssrdv 3938	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ (𝐴 ∩ 𝑥) = ∅)) → 𝑥 ⊆ ∩ 𝐴)
24		intss1 4911	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥)
25	24	ad2antrl 728	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ (𝐴 ∩ 𝑥) = ∅)) → ∩ 𝐴 ⊆ 𝑥)
26	23, 25	eqssd 3950	. . . . . . . . 9 ⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ (𝐴 ∩ 𝑥) = ∅)) → 𝑥 = ∩ 𝐴)
27	26	eleq1d 2814	. . . . . . . 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 3129	. . 3 ⊢ (𝐴 ⊆ On → (∃𝑥 ∈ 𝐴 (𝐴 ∩ 𝑥) = ∅ → ∩ 𝐴 ∈ 𝐴))
33	3, 32	syl5 34	. 2 ⊢ (𝐴 ⊆ On → ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝐴))
34	33	anabsi5 669	1 ⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2110   ≠ wne 2926  ∀wral 3045  ∃wrex 3054   ∩ cin 3899   ⊆ wss 3900  ∅c0 4281  ∩ cint 4895  Ord word 6301  Oncon0 6302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-pss 3920  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-int 4896  df-br 5090  df-opab 5152  df-tr 5197  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-ord 6305  df-on 6306

This theorem is referenced by:  onint0  7719  onssmin  7720  onminesb  7721  onminsb  7722  oninton  7723  oneqmin  7728  oeeulem  8511  nnawordex  8547  unblem1  9171  unblem2  9172  tz9.12lem3  9674  scott0  9771  cardid2  9838  ackbij1lem18  10119  cardcf  10135  cff1  10141  cflim2  10146  cfss  10148  cofsmo  10152  fin23lem26  10208  pwfseqlem3  10543  gruina  10701  2ndcdisj  23364  sltval2  27588  nobdaymin  27709  lrrecfr  27879  rankeq1o  36184  dnnumch3  43059  oninfint  43248  inaex  44309