MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rankunb Structured version   Visualization version   GIF version

Theorem rankunb 9268
Description: The rank of the union of two sets. Theorem 15.17(iii) of [Monk1] p. 112. (Contributed by Mario Carneiro, 10-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
rankunb ((𝐴 (𝑅1 “ On) ∧ 𝐵 (𝑅1 “ On)) → (rank‘(𝐴𝐵)) = ((rank‘𝐴) ∪ (rank‘𝐵)))

Proof of Theorem rankunb
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 unwf 9228 . . . . . . 7 ((𝐴 (𝑅1 “ On) ∧ 𝐵 (𝑅1 “ On)) ↔ (𝐴𝐵) ∈ (𝑅1 “ On))
2 rankval3b 9244 . . . . . . 7 ((𝐴𝐵) ∈ (𝑅1 “ On) → (rank‘(𝐴𝐵)) = {𝑦 ∈ On ∣ ∀𝑥 ∈ (𝐴𝐵)(rank‘𝑥) ∈ 𝑦})
31, 2sylbi 218 . . . . . 6 ((𝐴 (𝑅1 “ On) ∧ 𝐵 (𝑅1 “ On)) → (rank‘(𝐴𝐵)) = {𝑦 ∈ On ∣ ∀𝑥 ∈ (𝐴𝐵)(rank‘𝑥) ∈ 𝑦})
43eleq2d 2903 . . . . 5 ((𝐴 (𝑅1 “ On) ∧ 𝐵 (𝑅1 “ On)) → (𝑥 ∈ (rank‘(𝐴𝐵)) ↔ 𝑥 {𝑦 ∈ On ∣ ∀𝑥 ∈ (𝐴𝐵)(rank‘𝑥) ∈ 𝑦}))
5 vex 3503 . . . . . 6 𝑥 ∈ V
65elintrab 4886 . . . . 5 (𝑥 {𝑦 ∈ On ∣ ∀𝑥 ∈ (𝐴𝐵)(rank‘𝑥) ∈ 𝑦} ↔ ∀𝑦 ∈ On (∀𝑥 ∈ (𝐴𝐵)(rank‘𝑥) ∈ 𝑦𝑥𝑦))
74, 6syl6bb 288 . . . 4 ((𝐴 (𝑅1 “ On) ∧ 𝐵 (𝑅1 “ On)) → (𝑥 ∈ (rank‘(𝐴𝐵)) ↔ ∀𝑦 ∈ On (∀𝑥 ∈ (𝐴𝐵)(rank‘𝑥) ∈ 𝑦𝑥𝑦)))
8 elun 4129 . . . . . . 7 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
9 rankelb 9242 . . . . . . . . 9 (𝐴 (𝑅1 “ On) → (𝑥𝐴 → (rank‘𝑥) ∈ (rank‘𝐴)))
10 elun1 4156 . . . . . . . . 9 ((rank‘𝑥) ∈ (rank‘𝐴) → (rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵)))
119, 10syl6 35 . . . . . . . 8 (𝐴 (𝑅1 “ On) → (𝑥𝐴 → (rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵))))
12 rankelb 9242 . . . . . . . . 9 (𝐵 (𝑅1 “ On) → (𝑥𝐵 → (rank‘𝑥) ∈ (rank‘𝐵)))
13 elun2 4157 . . . . . . . . 9 ((rank‘𝑥) ∈ (rank‘𝐵) → (rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵)))
1412, 13syl6 35 . . . . . . . 8 (𝐵 (𝑅1 “ On) → (𝑥𝐵 → (rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵))))
1511, 14jaao 950 . . . . . . 7 ((𝐴 (𝑅1 “ On) ∧ 𝐵 (𝑅1 “ On)) → ((𝑥𝐴𝑥𝐵) → (rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵))))
168, 15syl5bi 243 . . . . . 6 ((𝐴 (𝑅1 “ On) ∧ 𝐵 (𝑅1 “ On)) → (𝑥 ∈ (𝐴𝐵) → (rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵))))
1716ralrimiv 3186 . . . . 5 ((𝐴 (𝑅1 “ On) ∧ 𝐵 (𝑅1 “ On)) → ∀𝑥 ∈ (𝐴𝐵)(rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵)))
18 rankon 9213 . . . . . . 7 (rank‘𝐴) ∈ On
19 rankon 9213 . . . . . . 7 (rank‘𝐵) ∈ On
2018, 19onun2i 6304 . . . . . 6 ((rank‘𝐴) ∪ (rank‘𝐵)) ∈ On
21 eleq2 2906 . . . . . . . . 9 (𝑦 = ((rank‘𝐴) ∪ (rank‘𝐵)) → ((rank‘𝑥) ∈ 𝑦 ↔ (rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵))))
2221ralbidv 3202 . . . . . . . 8 (𝑦 = ((rank‘𝐴) ∪ (rank‘𝐵)) → (∀𝑥 ∈ (𝐴𝐵)(rank‘𝑥) ∈ 𝑦 ↔ ∀𝑥 ∈ (𝐴𝐵)(rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵))))
23 eleq2 2906 . . . . . . . 8 (𝑦 = ((rank‘𝐴) ∪ (rank‘𝐵)) → (𝑥𝑦𝑥 ∈ ((rank‘𝐴) ∪ (rank‘𝐵))))
2422, 23imbi12d 346 . . . . . . 7 (𝑦 = ((rank‘𝐴) ∪ (rank‘𝐵)) → ((∀𝑥 ∈ (𝐴𝐵)(rank‘𝑥) ∈ 𝑦𝑥𝑦) ↔ (∀𝑥 ∈ (𝐴𝐵)(rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵)) → 𝑥 ∈ ((rank‘𝐴) ∪ (rank‘𝐵)))))
2524rspcv 3622 . . . . . 6 (((rank‘𝐴) ∪ (rank‘𝐵)) ∈ On → (∀𝑦 ∈ On (∀𝑥 ∈ (𝐴𝐵)(rank‘𝑥) ∈ 𝑦𝑥𝑦) → (∀𝑥 ∈ (𝐴𝐵)(rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵)) → 𝑥 ∈ ((rank‘𝐴) ∪ (rank‘𝐵)))))
2620, 25ax-mp 5 . . . . 5 (∀𝑦 ∈ On (∀𝑥 ∈ (𝐴𝐵)(rank‘𝑥) ∈ 𝑦𝑥𝑦) → (∀𝑥 ∈ (𝐴𝐵)(rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵)) → 𝑥 ∈ ((rank‘𝐴) ∪ (rank‘𝐵))))
2717, 26syl5com 31 . . . 4 ((𝐴 (𝑅1 “ On) ∧ 𝐵 (𝑅1 “ On)) → (∀𝑦 ∈ On (∀𝑥 ∈ (𝐴𝐵)(rank‘𝑥) ∈ 𝑦𝑥𝑦) → 𝑥 ∈ ((rank‘𝐴) ∪ (rank‘𝐵))))
287, 27sylbid 241 . . 3 ((𝐴 (𝑅1 “ On) ∧ 𝐵 (𝑅1 “ On)) → (𝑥 ∈ (rank‘(𝐴𝐵)) → 𝑥 ∈ ((rank‘𝐴) ∪ (rank‘𝐵))))
2928ssrdv 3977 . 2 ((𝐴 (𝑅1 “ On) ∧ 𝐵 (𝑅1 “ On)) → (rank‘(𝐴𝐵)) ⊆ ((rank‘𝐴) ∪ (rank‘𝐵)))
30 ssun1 4152 . . . . 5 𝐴 ⊆ (𝐴𝐵)
31 rankssb 9266 . . . . 5 ((𝐴𝐵) ∈ (𝑅1 “ On) → (𝐴 ⊆ (𝐴𝐵) → (rank‘𝐴) ⊆ (rank‘(𝐴𝐵))))
3230, 31mpi 20 . . . 4 ((𝐴𝐵) ∈ (𝑅1 “ On) → (rank‘𝐴) ⊆ (rank‘(𝐴𝐵)))
33 ssun2 4153 . . . . 5 𝐵 ⊆ (𝐴𝐵)
34 rankssb 9266 . . . . 5 ((𝐴𝐵) ∈ (𝑅1 “ On) → (𝐵 ⊆ (𝐴𝐵) → (rank‘𝐵) ⊆ (rank‘(𝐴𝐵))))
3533, 34mpi 20 . . . 4 ((𝐴𝐵) ∈ (𝑅1 “ On) → (rank‘𝐵) ⊆ (rank‘(𝐴𝐵)))
3632, 35unssd 4166 . . 3 ((𝐴𝐵) ∈ (𝑅1 “ On) → ((rank‘𝐴) ∪ (rank‘𝐵)) ⊆ (rank‘(𝐴𝐵)))
371, 36sylbi 218 . 2 ((𝐴 (𝑅1 “ On) ∧ 𝐵 (𝑅1 “ On)) → ((rank‘𝐴) ∪ (rank‘𝐵)) ⊆ (rank‘(𝐴𝐵)))
3829, 37eqssd 3988 1 ((𝐴 (𝑅1 “ On) ∧ 𝐵 (𝑅1 “ On)) → (rank‘(𝐴𝐵)) = ((rank‘𝐴) ∪ (rank‘𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wo 843   = wceq 1530  wcel 2107  wral 3143  {crab 3147  cun 3938  wss 3940   cuni 4837   cint 4874  cima 5557  Oncon0 6189  cfv 6352  𝑅1cr1 9180  rankcrnk 9181
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6146  df-ord 6192  df-on 6193  df-lim 6194  df-suc 6195  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-om 7569  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-r1 9182  df-rank 9183
This theorem is referenced by:  rankprb  9269  rankopb  9270  rankun  9274  rankaltopb  33324
  Copyright terms: Public domain W3C validator