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

Theorem djuen 7015
Description: Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.)
Assertion
Ref Expression
djuen ((𝐴𝐵𝐶𝐷) → (𝐴𝐶) ≈ (𝐵𝐷))

Proof of Theorem djuen
StepHypRef Expression
1 encv 6594 . . . . . . . 8 (𝐴𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
21adantr 272 . . . . . . 7 ((𝐴𝐵𝐶𝐷) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
32simpld 111 . . . . . 6 ((𝐴𝐵𝐶𝐷) → 𝐴 ∈ V)
4 eninl 6934 . . . . . 6 (𝐴 ∈ V → (inl “ 𝐴) ≈ 𝐴)
53, 4syl 14 . . . . 5 ((𝐴𝐵𝐶𝐷) → (inl “ 𝐴) ≈ 𝐴)
6 simpl 108 . . . . 5 ((𝐴𝐵𝐶𝐷) → 𝐴𝐵)
7 entr 6632 . . . . 5 (((inl “ 𝐴) ≈ 𝐴𝐴𝐵) → (inl “ 𝐴) ≈ 𝐵)
85, 6, 7syl2anc 406 . . . 4 ((𝐴𝐵𝐶𝐷) → (inl “ 𝐴) ≈ 𝐵)
9 eninl 6934 . . . . . 6 (𝐵 ∈ V → (inl “ 𝐵) ≈ 𝐵)
102, 9simpl2im 381 . . . . 5 ((𝐴𝐵𝐶𝐷) → (inl “ 𝐵) ≈ 𝐵)
1110ensymd 6631 . . . 4 ((𝐴𝐵𝐶𝐷) → 𝐵 ≈ (inl “ 𝐵))
12 entr 6632 . . . 4 (((inl “ 𝐴) ≈ 𝐵𝐵 ≈ (inl “ 𝐵)) → (inl “ 𝐴) ≈ (inl “ 𝐵))
138, 11, 12syl2anc 406 . . 3 ((𝐴𝐵𝐶𝐷) → (inl “ 𝐴) ≈ (inl “ 𝐵))
14 encv 6594 . . . . . . . 8 (𝐶𝐷 → (𝐶 ∈ V ∧ 𝐷 ∈ V))
1514adantl 273 . . . . . . 7 ((𝐴𝐵𝐶𝐷) → (𝐶 ∈ V ∧ 𝐷 ∈ V))
1615simpld 111 . . . . . 6 ((𝐴𝐵𝐶𝐷) → 𝐶 ∈ V)
17 eninr 6935 . . . . . 6 (𝐶 ∈ V → (inr “ 𝐶) ≈ 𝐶)
1816, 17syl 14 . . . . 5 ((𝐴𝐵𝐶𝐷) → (inr “ 𝐶) ≈ 𝐶)
19 entr 6632 . . . . 5 (((inr “ 𝐶) ≈ 𝐶𝐶𝐷) → (inr “ 𝐶) ≈ 𝐷)
2018, 19sylancom 414 . . . 4 ((𝐴𝐵𝐶𝐷) → (inr “ 𝐶) ≈ 𝐷)
21 eninr 6935 . . . . . 6 (𝐷 ∈ V → (inr “ 𝐷) ≈ 𝐷)
2215, 21simpl2im 381 . . . . 5 ((𝐴𝐵𝐶𝐷) → (inr “ 𝐷) ≈ 𝐷)
2322ensymd 6631 . . . 4 ((𝐴𝐵𝐶𝐷) → 𝐷 ≈ (inr “ 𝐷))
24 entr 6632 . . . 4 (((inr “ 𝐶) ≈ 𝐷𝐷 ≈ (inr “ 𝐷)) → (inr “ 𝐶) ≈ (inr “ 𝐷))
2520, 23, 24syl2anc 406 . . 3 ((𝐴𝐵𝐶𝐷) → (inr “ 𝐶) ≈ (inr “ 𝐷))
26 djuin 6901 . . . 4 ((inl “ 𝐴) ∩ (inr “ 𝐶)) = ∅
2726a1i 9 . . 3 ((𝐴𝐵𝐶𝐷) → ((inl “ 𝐴) ∩ (inr “ 𝐶)) = ∅)
28 djuin 6901 . . . 4 ((inl “ 𝐵) ∩ (inr “ 𝐷)) = ∅
2928a1i 9 . . 3 ((𝐴𝐵𝐶𝐷) → ((inl “ 𝐵) ∩ (inr “ 𝐷)) = ∅)
30 unen 6664 . . 3 ((((inl “ 𝐴) ≈ (inl “ 𝐵) ∧ (inr “ 𝐶) ≈ (inr “ 𝐷)) ∧ (((inl “ 𝐴) ∩ (inr “ 𝐶)) = ∅ ∧ ((inl “ 𝐵) ∩ (inr “ 𝐷)) = ∅)) → ((inl “ 𝐴) ∪ (inr “ 𝐶)) ≈ ((inl “ 𝐵) ∪ (inr “ 𝐷)))
3113, 25, 27, 29, 30syl22anc 1200 . 2 ((𝐴𝐵𝐶𝐷) → ((inl “ 𝐴) ∪ (inr “ 𝐶)) ≈ ((inl “ 𝐵) ∪ (inr “ 𝐷)))
32 djuun 6904 . 2 ((inl “ 𝐴) ∪ (inr “ 𝐶)) = (𝐴𝐶)
33 djuun 6904 . 2 ((inl “ 𝐵) ∪ (inr “ 𝐷)) = (𝐵𝐷)
3431, 32, 333brtr3g 3926 1 ((𝐴𝐵𝐶𝐷) → (𝐴𝐶) ≈ (𝐵𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1314  wcel 1463  Vcvv 2657  cun 3035  cin 3036  c0 3329   class class class wbr 3895  cima 4502  cen 6586  cdju 6874  inlcinl 6882  inrcinr 6883
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4003  ax-sep 4006  ax-nul 4014  ax-pow 4058  ax-pr 4091  ax-un 4315
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-ne 2283  df-ral 2395  df-rex 2396  df-reu 2397  df-rab 2399  df-v 2659  df-sbc 2879  df-csb 2972  df-dif 3039  df-un 3041  df-in 3043  df-ss 3050  df-nul 3330  df-pw 3478  df-sn 3499  df-pr 3500  df-op 3502  df-uni 3703  df-iun 3781  df-br 3896  df-opab 3950  df-mpt 3951  df-tr 3987  df-id 4175  df-iord 4248  df-on 4250  df-suc 4253  df-xp 4505  df-rel 4506  df-cnv 4507  df-co 4508  df-dm 4509  df-rn 4510  df-res 4511  df-ima 4512  df-iota 5046  df-fun 5083  df-fn 5084  df-f 5085  df-f1 5086  df-fo 5087  df-f1o 5088  df-fv 5089  df-1st 5992  df-2nd 5993  df-1o 6267  df-er 6383  df-en 6589  df-dju 6875  df-inl 6884  df-inr 6885
This theorem is referenced by:  djuenun  7016  exmidunben  11784
  Copyright terms: Public domain W3C validator