Theorem brfvrcld2 38755

Description: If two elements are connected by the reflexive closure of a relation, then they are equal or related by relation. (Contributed by RP, 21-Jul-2020.)

Hypothesis

Ref	Expression
brfvrcld2.r	⊢ (𝜑 → 𝑅 ∈ V)

Assertion

Ref	Expression
brfvrcld2	⊢ (𝜑 → (𝐴(r*‘𝑅)𝐵 ↔ ((𝐴 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐵 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐴 = 𝐵) ∨ 𝐴𝑅𝐵)))

Proof of Theorem brfvrcld2

Step	Hyp	Ref	Expression
1		brfvrcld2.r	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
2	1	brfvrcld 38754	. 2 ⊢ (𝜑 → (𝐴(r*‘𝑅)𝐵 ↔ (𝐴(𝑅↑𝑟0)𝐵 ∨ 𝐴(𝑅↑𝑟1)𝐵)))
3		relexp0g 14100	. . . . . 6 ⊢ (𝑅 ∈ V → (𝑅↑𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
4	1, 3	syl 17	. . . . 5 ⊢ (𝜑 → (𝑅↑𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
5	4	breqd 4852	. . . 4 ⊢ (𝜑 → (𝐴(𝑅↑𝑟0)𝐵 ↔ 𝐴( I ↾ (dom 𝑅 ∪ ran 𝑅))𝐵))
6		relres 5634	. . . . . . . 8 ⊢ Rel ( I ↾ (dom 𝑅 ∪ ran 𝑅))
7	6	releldmi 5564	. . . . . . 7 ⊢ (𝐴( I ↾ (dom 𝑅 ∪ ran 𝑅))𝐵 → 𝐴 ∈ dom ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
8	6	relelrni 5565	. . . . . . 7 ⊢ (𝐴( I ↾ (dom 𝑅 ∪ ran 𝑅))𝐵 → 𝐵 ∈ ran ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
9		dmresi 5674	. . . . . . . . . 10 ⊢ dom ( I ↾ (dom 𝑅 ∪ ran 𝑅)) = (dom 𝑅 ∪ ran 𝑅)
10	9	eleq2i 2868	. . . . . . . . 9 ⊢ (𝐴 ∈ dom ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ↔ 𝐴 ∈ (dom 𝑅 ∪ ran 𝑅))
11	10	biimpi 208	. . . . . . . 8 ⊢ (𝐴 ∈ dom ( I ↾ (dom 𝑅 ∪ ran 𝑅)) → 𝐴 ∈ (dom 𝑅 ∪ ran 𝑅))
12		rnresi 5694	. . . . . . . . . 10 ⊢ ran ( I ↾ (dom 𝑅 ∪ ran 𝑅)) = (dom 𝑅 ∪ ran 𝑅)
13	12	eleq2i 2868	. . . . . . . . 9 ⊢ (𝐵 ∈ ran ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ↔ 𝐵 ∈ (dom 𝑅 ∪ ran 𝑅))
14	13	biimpi 208	. . . . . . . 8 ⊢ (𝐵 ∈ ran ( I ↾ (dom 𝑅 ∪ ran 𝑅)) → 𝐵 ∈ (dom 𝑅 ∪ ran 𝑅))
15	11, 14	anim12i 607	. . . . . . 7 ⊢ ((𝐴 ∈ dom ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ∧ 𝐵 ∈ ran ( I ↾ (dom 𝑅 ∪ ran 𝑅))) → (𝐴 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐵 ∈ (dom 𝑅 ∪ ran 𝑅)))
16	7, 8, 15	syl2anc 580	. . . . . 6 ⊢ (𝐴( I ↾ (dom 𝑅 ∪ ran 𝑅))𝐵 → (𝐴 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐵 ∈ (dom 𝑅 ∪ ran 𝑅)))
17		resieq 5616	. . . . . 6 ⊢ ((𝐴 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐵 ∈ (dom 𝑅 ∪ ran 𝑅)) → (𝐴( I ↾ (dom 𝑅 ∪ ran 𝑅))𝐵 ↔ 𝐴 = 𝐵))
18	16, 17	biadan2 854	. . . . 5 ⊢ (𝐴( I ↾ (dom 𝑅 ∪ ran 𝑅))𝐵 ↔ ((𝐴 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐵 ∈ (dom 𝑅 ∪ ran 𝑅)) ∧ 𝐴 = 𝐵))
19		df-3an 1110	. . . . 5 ⊢ ((𝐴 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐵 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐴 = 𝐵) ↔ ((𝐴 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐵 ∈ (dom 𝑅 ∪ ran 𝑅)) ∧ 𝐴 = 𝐵))
20	18, 19	bitr4i 270	. . . 4 ⊢ (𝐴( I ↾ (dom 𝑅 ∪ ran 𝑅))𝐵 ↔ (𝐴 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐵 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐴 = 𝐵))
21	5, 20	syl6bb 279	. . 3 ⊢ (𝜑 → (𝐴(𝑅↑𝑟0)𝐵 ↔ (𝐴 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐵 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐴 = 𝐵)))
22	1	relexp1d 14109	. . . 4 ⊢ (𝜑 → (𝑅↑𝑟1) = 𝑅)
23	22	breqd 4852	. . 3 ⊢ (𝜑 → (𝐴(𝑅↑𝑟1)𝐵 ↔ 𝐴𝑅𝐵))
24	21, 23	orbi12d 943	. 2 ⊢ (𝜑 → ((𝐴(𝑅↑𝑟0)𝐵 ∨ 𝐴(𝑅↑𝑟1)𝐵) ↔ ((𝐴 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐵 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐴 = 𝐵) ∨ 𝐴𝑅𝐵)))
25	2, 24	bitrd 271	1 ⊢ (𝜑 → (𝐴(r*‘𝑅)𝐵 ↔ ((𝐴 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐵 ∈ (dom 𝑅 ∪ ran 𝑅) ∧ 𝐴 = 𝐵) ∨ 𝐴𝑅𝐵)))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 385   ∨ wo 874   ∧ w3a 1108   = wceq 1653   ∈ wcel 2157  Vcvv 3383   ∪ cun 3765   class class class wbr 4841   I cid 5217  dom cdm 5310  ran crn 5311   ↾ cres 5312  ‘cfv 6099  (class class class)co 6876  0cc0 10222  1c1 10223  ↑_𝑟crelexp 14098  r*crcl 38735

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-ext 2775  ax-rep 4962  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5095  ax-un 7181  ax-cnex 10278  ax-resscn 10279  ax-1cn 10280  ax-icn 10281  ax-addcl 10282  ax-addrcl 10283  ax-mulcl 10284  ax-mulrcl 10285  ax-mulcom 10286  ax-addass 10287  ax-mulass 10288  ax-distr 10289  ax-i2m1 10290  ax-1ne0 10291  ax-1rid 10292  ax-rnegex 10293  ax-rrecex 10294  ax-cnre 10295  ax-pre-lttri 10296  ax-pre-lttrn 10297  ax-pre-ltadd 10298  ax-pre-mulgt0 10299

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2590  df-eu 2607  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ne 2970  df-nel 3073  df-ral 3092  df-rex 3093  df-reu 3094  df-rab 3096  df-v 3385  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-pss 3783  df-nul 4114  df-if 4276  df-pw 4349  df-sn 4367  df-pr 4369  df-tp 4371  df-op 4373  df-uni 4627  df-int 4666  df-iun 4710  df-br 4842  df-opab 4904  df-mpt 4921  df-tr 4944  df-id 5218  df-eprel 5223  df-po 5231  df-so 5232  df-fr 5269  df-we 5271  df-xp 5316  df-rel 5317  df-cnv 5318  df-co 5319  df-dm 5320  df-rn 5321  df-res 5322  df-ima 5323  df-pred 5896  df-ord 5942  df-on 5943  df-lim 5944  df-suc 5945  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-f1 6104  df-fo 6105  df-f1o 6106  df-fv 6107  df-riota 6837  df-ov 6879  df-oprab 6880  df-mpt2 6881  df-om 7298  df-2nd 7400  df-wrecs 7643  df-recs 7705  df-rdg 7743  df-er 7980  df-en 8194  df-dom 8195  df-sdom 8196  df-pnf 10363  df-mnf 10364  df-xr 10365  df-ltxr 10366  df-le 10367  df-sub 10556  df-neg 10557  df-nn 11311  df-n0 11577  df-z 11663  df-uz 11927  df-seq 13052  df-relexp 14099  df-rcl 38736

This theorem is referenced by: (None)