ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  onintonm GIF version

Theorem onintonm 4499
Description: The intersection of an inhabited collection of ordinal numbers is an ordinal number. Compare Exercise 6 of [TakeutiZaring] p. 44. (Contributed by Mario Carneiro and Jim Kingdon, 30-Aug-2021.)
Assertion
Ref Expression
onintonm ((𝐴 ⊆ On ∧ ∃𝑥 𝑥𝐴) → 𝐴 ∈ On)
Distinct variable group:   𝑥,𝐴

Proof of Theorem onintonm
StepHypRef Expression
1 ssel 3141 . . . . . . 7 (𝐴 ⊆ On → (𝑥𝐴𝑥 ∈ On))
2 eloni 4358 . . . . . . . 8 (𝑥 ∈ On → Ord 𝑥)
3 ordtr 4361 . . . . . . . 8 (Ord 𝑥 → Tr 𝑥)
42, 3syl 14 . . . . . . 7 (𝑥 ∈ On → Tr 𝑥)
51, 4syl6 33 . . . . . 6 (𝐴 ⊆ On → (𝑥𝐴 → Tr 𝑥))
65ralrimiv 2542 . . . . 5 (𝐴 ⊆ On → ∀𝑥𝐴 Tr 𝑥)
7 trint 4100 . . . . 5 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
86, 7syl 14 . . . 4 (𝐴 ⊆ On → Tr 𝐴)
98adantr 274 . . 3 ((𝐴 ⊆ On ∧ ∃𝑥 𝑥𝐴) → Tr 𝐴)
10 nfv 1521 . . . . 5 𝑥 𝐴 ⊆ On
11 nfe1 1489 . . . . 5 𝑥𝑥 𝑥𝐴
1210, 11nfan 1558 . . . 4 𝑥(𝐴 ⊆ On ∧ ∃𝑥 𝑥𝐴)
13 intssuni2m 3853 . . . . . . . 8 ((𝐴 ⊆ On ∧ ∃𝑥 𝑥𝐴) → 𝐴 On)
14 unon 4493 . . . . . . . 8 On = On
1513, 14sseqtrdi 3195 . . . . . . 7 ((𝐴 ⊆ On ∧ ∃𝑥 𝑥𝐴) → 𝐴 ⊆ On)
1615sseld 3146 . . . . . 6 ((𝐴 ⊆ On ∧ ∃𝑥 𝑥𝐴) → (𝑥 𝐴𝑥 ∈ On))
1716, 2syl6 33 . . . . 5 ((𝐴 ⊆ On ∧ ∃𝑥 𝑥𝐴) → (𝑥 𝐴 → Ord 𝑥))
1817, 3syl6 33 . . . 4 ((𝐴 ⊆ On ∧ ∃𝑥 𝑥𝐴) → (𝑥 𝐴 → Tr 𝑥))
1912, 18ralrimi 2541 . . 3 ((𝐴 ⊆ On ∧ ∃𝑥 𝑥𝐴) → ∀𝑥 𝐴Tr 𝑥)
20 dford3 4350 . . 3 (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 𝐴Tr 𝑥))
219, 19, 20sylanbrc 415 . 2 ((𝐴 ⊆ On ∧ ∃𝑥 𝑥𝐴) → Ord 𝐴)
22 inteximm 4133 . . . 4 (∃𝑥 𝑥𝐴 𝐴 ∈ V)
2322adantl 275 . . 3 ((𝐴 ⊆ On ∧ ∃𝑥 𝑥𝐴) → 𝐴 ∈ V)
24 elong 4356 . . 3 ( 𝐴 ∈ V → ( 𝐴 ∈ On ↔ Ord 𝐴))
2523, 24syl 14 . 2 ((𝐴 ⊆ On ∧ ∃𝑥 𝑥𝐴) → ( 𝐴 ∈ On ↔ Ord 𝐴))
2621, 25mpbird 166 1 ((𝐴 ⊆ On ∧ ∃𝑥 𝑥𝐴) → 𝐴 ∈ On)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wex 1485  wcel 2141  wral 2448  Vcvv 2730  wss 3121   cuni 3794   cint 3829  Tr wtr 4085  Ord word 4345  Oncon0 4346
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4105  ax-pow 4158  ax-pr 4192  ax-un 4416
This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-pw 3566  df-sn 3587  df-pr 3588  df-uni 3795  df-int 3830  df-tr 4086  df-iord 4349  df-on 4351  df-suc 4354
This theorem is referenced by:  onintrab2im  4500
  Copyright terms: Public domain W3C validator