Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rfovcnvf1od Structured version   Visualization version   GIF version

Theorem rfovcnvf1od 42350
Description: Properties of the operator, (𝐴𝑂𝐡), which maps between relations and functions for relations between base sets, 𝐴 and 𝐡. (Contributed by RP, 27-Apr-2021.)
Hypotheses
Ref Expression
rfovd.rf 𝑂 = (π‘Ž ∈ V, 𝑏 ∈ V ↦ (π‘Ÿ ∈ 𝒫 (π‘Ž Γ— 𝑏) ↦ (π‘₯ ∈ π‘Ž ↦ {𝑦 ∈ 𝑏 ∣ π‘₯π‘Ÿπ‘¦})))
rfovd.a (πœ‘ β†’ 𝐴 ∈ 𝑉)
rfovd.b (πœ‘ β†’ 𝐡 ∈ π‘Š)
rfovcnvf1od.f 𝐹 = (𝐴𝑂𝐡)
Assertion
Ref Expression
rfovcnvf1od (πœ‘ β†’ (𝐹:𝒫 (𝐴 Γ— 𝐡)–1-1-ontoβ†’(𝒫 𝐡 ↑m 𝐴) ∧ ◑𝐹 = (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))})))
Distinct variable groups:   𝐴,π‘Ž,𝑏,𝑓,π‘Ÿ,π‘₯,𝑦   𝐡,π‘Ž,𝑏,𝑓,π‘Ÿ,π‘₯,𝑦   π‘Š,π‘Ž,π‘₯   πœ‘,π‘Ž,𝑏,𝑓,π‘Ÿ,π‘₯,𝑦
Allowed substitution hints:   𝐹(π‘₯,𝑦,𝑓,π‘Ÿ,π‘Ž,𝑏)   𝑂(π‘₯,𝑦,𝑓,π‘Ÿ,π‘Ž,𝑏)   𝑉(π‘₯,𝑦,𝑓,π‘Ÿ,π‘Ž,𝑏)   π‘Š(𝑦,𝑓,π‘Ÿ,𝑏)

Proof of Theorem rfovcnvf1od
Dummy variables 𝑒 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2737 . . 3 (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) = (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦}))
2 rfovd.b . . . . . . . 8 (πœ‘ β†’ 𝐡 ∈ π‘Š)
3 ssrab2 4042 . . . . . . . . 9 {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦} βŠ† 𝐡
43a1i 11 . . . . . . . 8 (πœ‘ β†’ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦} βŠ† 𝐡)
52, 4sselpwd 5288 . . . . . . 7 (πœ‘ β†’ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦} ∈ 𝒫 𝐡)
65adantr 482 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦} ∈ 𝒫 𝐡)
76fmpttd 7068 . . . . 5 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦}):π΄βŸΆπ’« 𝐡)
82pwexd 5339 . . . . . 6 (πœ‘ β†’ 𝒫 𝐡 ∈ V)
9 rfovd.a . . . . . 6 (πœ‘ β†’ 𝐴 ∈ 𝑉)
108, 9elmapd 8786 . . . . 5 (πœ‘ β†’ ((π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦}) ∈ (𝒫 𝐡 ↑m 𝐴) ↔ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦}):π΄βŸΆπ’« 𝐡))
117, 10mpbird 257 . . . 4 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦}) ∈ (𝒫 𝐡 ↑m 𝐴))
1211adantr 482 . . 3 ((πœ‘ ∧ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡)) β†’ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦}) ∈ (𝒫 𝐡 ↑m 𝐴))
139, 2xpexd 7690 . . . . 5 (πœ‘ β†’ (𝐴 Γ— 𝐡) ∈ V)
1413adantr 482 . . . 4 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ (𝐴 Γ— 𝐡) ∈ V)
158, 9elmapd 8786 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↔ 𝑓:π΄βŸΆπ’« 𝐡))
1615biimpa 478 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ 𝑓:π΄βŸΆπ’« 𝐡)
1716ffvelcdmda 7040 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) ∧ π‘₯ ∈ 𝐴) β†’ (π‘“β€˜π‘₯) ∈ 𝒫 𝐡)
1817ex 414 . . . . . . . . 9 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ (π‘₯ ∈ 𝐴 β†’ (π‘“β€˜π‘₯) ∈ 𝒫 𝐡))
19 elpwi 4572 . . . . . . . . . 10 ((π‘“β€˜π‘₯) ∈ 𝒫 𝐡 β†’ (π‘“β€˜π‘₯) βŠ† 𝐡)
2019sseld 3948 . . . . . . . . 9 ((π‘“β€˜π‘₯) ∈ 𝒫 𝐡 β†’ (𝑦 ∈ (π‘“β€˜π‘₯) β†’ 𝑦 ∈ 𝐡))
2118, 20syl6 35 . . . . . . . 8 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ (π‘₯ ∈ 𝐴 β†’ (𝑦 ∈ (π‘“β€˜π‘₯) β†’ 𝑦 ∈ 𝐡)))
2221imdistand 572 . . . . . . 7 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯)) β†’ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐡)))
23 trud 1552 . . . . . . 7 ((π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯)) β†’ ⊀)
2422, 23jca2 515 . . . . . 6 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯)) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐡) ∧ ⊀)))
2524ssopab2dv 5513 . . . . 5 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))} βŠ† {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐡) ∧ ⊀)})
26 opabssxp 5729 . . . . 5 {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐡) ∧ ⊀)} βŠ† (𝐴 Γ— 𝐡)
2725, 26sstrdi 3961 . . . 4 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))} βŠ† (𝐴 Γ— 𝐡))
2814, 27sselpwd 5288 . . 3 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))} ∈ 𝒫 (𝐴 Γ— 𝐡))
29 simplrr 777 . . . . . 6 (((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) β†’ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))
30 elmapfn 8810 . . . . . 6 (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) β†’ 𝑓 Fn 𝐴)
3129, 30syl 17 . . . . 5 (((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) β†’ 𝑓 Fn 𝐴)
322ad2antrr 725 . . . . . 6 (((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) β†’ 𝐡 ∈ π‘Š)
33 rabexg 5293 . . . . . . 7 (𝐡 ∈ π‘Š β†’ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦} ∈ V)
3433ralrimivw 3148 . . . . . 6 (𝐡 ∈ π‘Š β†’ βˆ€π‘₯ ∈ 𝐴 {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦} ∈ V)
35 nfcv 2908 . . . . . . 7 β„²π‘₯𝐴
3635fnmptf 6642 . . . . . 6 (βˆ€π‘₯ ∈ 𝐴 {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦} ∈ V β†’ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦}) Fn 𝐴)
3732, 34, 363syl 18 . . . . 5 (((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) β†’ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦}) Fn 𝐴)
38 dfin5 3923 . . . . . . 7 (𝐡 ∩ (π‘“β€˜π‘’)) = {𝑏 ∈ 𝐡 ∣ 𝑏 ∈ (π‘“β€˜π‘’)}
39 simpllr 775 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ∧ 𝑒 ∈ 𝐴) β†’ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)))
40 elmapi 8794 . . . . . . . . . . 11 (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) β†’ 𝑓:π΄βŸΆπ’« 𝐡)
4139, 40simpl2im 505 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ∧ 𝑒 ∈ 𝐴) β†’ 𝑓:π΄βŸΆπ’« 𝐡)
42 simpr 486 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ∧ 𝑒 ∈ 𝐴) β†’ 𝑒 ∈ 𝐴)
4341, 42ffvelcdmd 7041 . . . . . . . . 9 ((((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ∧ 𝑒 ∈ 𝐴) β†’ (π‘“β€˜π‘’) ∈ 𝒫 𝐡)
4443elpwid 4574 . . . . . . . 8 ((((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ∧ 𝑒 ∈ 𝐴) β†’ (π‘“β€˜π‘’) βŠ† 𝐡)
45 sseqin2 4180 . . . . . . . 8 ((π‘“β€˜π‘’) βŠ† 𝐡 ↔ (𝐡 ∩ (π‘“β€˜π‘’)) = (π‘“β€˜π‘’))
4644, 45sylib 217 . . . . . . 7 ((((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ∧ 𝑒 ∈ 𝐴) β†’ (𝐡 ∩ (π‘“β€˜π‘’)) = (π‘“β€˜π‘’))
47 ibar 530 . . . . . . . . 9 (𝑒 ∈ 𝐴 β†’ (𝑏 ∈ (π‘“β€˜π‘’) ↔ (𝑒 ∈ 𝐴 ∧ 𝑏 ∈ (π‘“β€˜π‘’))))
4847rabbidv 3418 . . . . . . . 8 (𝑒 ∈ 𝐴 β†’ {𝑏 ∈ 𝐡 ∣ 𝑏 ∈ (π‘“β€˜π‘’)} = {𝑏 ∈ 𝐡 ∣ (𝑒 ∈ 𝐴 ∧ 𝑏 ∈ (π‘“β€˜π‘’))})
4948adantl 483 . . . . . . 7 ((((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ∧ 𝑒 ∈ 𝐴) β†’ {𝑏 ∈ 𝐡 ∣ 𝑏 ∈ (π‘“β€˜π‘’)} = {𝑏 ∈ 𝐡 ∣ (𝑒 ∈ 𝐴 ∧ 𝑏 ∈ (π‘“β€˜π‘’))})
5038, 46, 493eqtr3a 2801 . . . . . 6 ((((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ∧ 𝑒 ∈ 𝐴) β†’ (π‘“β€˜π‘’) = {𝑏 ∈ 𝐡 ∣ (𝑒 ∈ 𝐴 ∧ 𝑏 ∈ (π‘“β€˜π‘’))})
51 breq2 5114 . . . . . . . . . 10 (𝑦 = 𝑏 β†’ (π‘₯π‘Ÿπ‘¦ ↔ π‘₯π‘Ÿπ‘))
5251cbvrabv 3420 . . . . . . . . 9 {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦} = {𝑏 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘}
53 breq1 5113 . . . . . . . . . . 11 (π‘₯ = π‘Ž β†’ (π‘₯π‘Ÿπ‘ ↔ π‘Žπ‘Ÿπ‘))
54 df-br 5111 . . . . . . . . . . 11 (π‘Žπ‘Ÿπ‘ ↔ βŸ¨π‘Ž, π‘βŸ© ∈ π‘Ÿ)
5553, 54bitrdi 287 . . . . . . . . . 10 (π‘₯ = π‘Ž β†’ (π‘₯π‘Ÿπ‘ ↔ βŸ¨π‘Ž, π‘βŸ© ∈ π‘Ÿ))
5655rabbidv 3418 . . . . . . . . 9 (π‘₯ = π‘Ž β†’ {𝑏 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘} = {𝑏 ∈ 𝐡 ∣ βŸ¨π‘Ž, π‘βŸ© ∈ π‘Ÿ})
5752, 56eqtrid 2789 . . . . . . . 8 (π‘₯ = π‘Ž β†’ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦} = {𝑏 ∈ 𝐡 ∣ βŸ¨π‘Ž, π‘βŸ© ∈ π‘Ÿ})
5857cbvmptv 5223 . . . . . . 7 (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦}) = (π‘Ž ∈ 𝐴 ↦ {𝑏 ∈ 𝐡 ∣ βŸ¨π‘Ž, π‘βŸ© ∈ π‘Ÿ})
59 simpr 486 . . . . . . . . . . 11 (((((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ∧ 𝑒 ∈ 𝐴) ∧ π‘Ž = 𝑒) β†’ π‘Ž = 𝑒)
6059opeq1d 4841 . . . . . . . . . 10 (((((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ∧ 𝑒 ∈ 𝐴) ∧ π‘Ž = 𝑒) β†’ βŸ¨π‘Ž, π‘βŸ© = βŸ¨π‘’, π‘βŸ©)
61 simpllr 775 . . . . . . . . . 10 (((((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ∧ 𝑒 ∈ 𝐴) ∧ π‘Ž = 𝑒) β†’ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))})
6260, 61eleq12d 2832 . . . . . . . . 9 (((((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ∧ 𝑒 ∈ 𝐴) ∧ π‘Ž = 𝑒) β†’ (βŸ¨π‘Ž, π‘βŸ© ∈ π‘Ÿ ↔ βŸ¨π‘’, π‘βŸ© ∈ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}))
63 vex 3452 . . . . . . . . . 10 𝑒 ∈ V
64 vex 3452 . . . . . . . . . 10 𝑏 ∈ V
65 simpl 484 . . . . . . . . . . . 12 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑏) β†’ π‘₯ = 𝑒)
6665eleq1d 2823 . . . . . . . . . . 11 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑏) β†’ (π‘₯ ∈ 𝐴 ↔ 𝑒 ∈ 𝐴))
67 simpr 486 . . . . . . . . . . . 12 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑏) β†’ 𝑦 = 𝑏)
6865fveq2d 6851 . . . . . . . . . . . 12 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑏) β†’ (π‘“β€˜π‘₯) = (π‘“β€˜π‘’))
6967, 68eleq12d 2832 . . . . . . . . . . 11 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑏) β†’ (𝑦 ∈ (π‘“β€˜π‘₯) ↔ 𝑏 ∈ (π‘“β€˜π‘’)))
7066, 69anbi12d 632 . . . . . . . . . 10 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑏) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯)) ↔ (𝑒 ∈ 𝐴 ∧ 𝑏 ∈ (π‘“β€˜π‘’))))
7163, 64, 70opelopaba 5498 . . . . . . . . 9 (βŸ¨π‘’, π‘βŸ© ∈ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))} ↔ (𝑒 ∈ 𝐴 ∧ 𝑏 ∈ (π‘“β€˜π‘’)))
7262, 71bitrdi 287 . . . . . . . 8 (((((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ∧ 𝑒 ∈ 𝐴) ∧ π‘Ž = 𝑒) β†’ (βŸ¨π‘Ž, π‘βŸ© ∈ π‘Ÿ ↔ (𝑒 ∈ 𝐴 ∧ 𝑏 ∈ (π‘“β€˜π‘’))))
7372rabbidv 3418 . . . . . . 7 (((((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ∧ 𝑒 ∈ 𝐴) ∧ π‘Ž = 𝑒) β†’ {𝑏 ∈ 𝐡 ∣ βŸ¨π‘Ž, π‘βŸ© ∈ π‘Ÿ} = {𝑏 ∈ 𝐡 ∣ (𝑒 ∈ 𝐴 ∧ 𝑏 ∈ (π‘“β€˜π‘’))})
742ad3antrrr 729 . . . . . . . 8 ((((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ∧ 𝑒 ∈ 𝐴) β†’ 𝐡 ∈ π‘Š)
75 rabexg 5293 . . . . . . . 8 (𝐡 ∈ π‘Š β†’ {𝑏 ∈ 𝐡 ∣ (𝑒 ∈ 𝐴 ∧ 𝑏 ∈ (π‘“β€˜π‘’))} ∈ V)
7674, 75syl 17 . . . . . . 7 ((((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ∧ 𝑒 ∈ 𝐴) β†’ {𝑏 ∈ 𝐡 ∣ (𝑒 ∈ 𝐴 ∧ 𝑏 ∈ (π‘“β€˜π‘’))} ∈ V)
7758, 73, 42, 76fvmptd2 6961 . . . . . 6 ((((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ∧ 𝑒 ∈ 𝐴) β†’ ((π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})β€˜π‘’) = {𝑏 ∈ 𝐡 ∣ (𝑒 ∈ 𝐴 ∧ 𝑏 ∈ (π‘“β€˜π‘’))})
7850, 77eqtr4d 2780 . . . . 5 ((((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ∧ 𝑒 ∈ 𝐴) β†’ (π‘“β€˜π‘’) = ((π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})β€˜π‘’))
7931, 37, 78eqfnfvd 6990 . . . 4 (((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) β†’ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦}))
80 simplrl 776 . . . . . . . 8 (((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) β†’ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡))
8180elpwid 4574 . . . . . . 7 (((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) β†’ π‘Ÿ βŠ† (𝐴 Γ— 𝐡))
82 xpss 5654 . . . . . . 7 (𝐴 Γ— 𝐡) βŠ† (V Γ— V)
8381, 82sstrdi 3961 . . . . . 6 (((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) β†’ π‘Ÿ βŠ† (V Γ— V))
84 df-rel 5645 . . . . . 6 (Rel π‘Ÿ ↔ π‘Ÿ βŠ† (V Γ— V))
8583, 84sylibr 233 . . . . 5 (((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) β†’ Rel π‘Ÿ)
86 relopabv 5782 . . . . . 6 Rel {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}
8786a1i 11 . . . . 5 (((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) β†’ Rel {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))})
88 simpl 484 . . . . . . 7 ((π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴)) β†’ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡))
892, 88anim12i 614 . . . . . 6 ((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) β†’ (𝐡 ∈ π‘Š ∧ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡)))
9089anim1i 616 . . . . 5 (((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) β†’ ((𝐡 ∈ π‘Š ∧ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡)) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})))
91 vex 3452 . . . . . . . 8 𝑣 ∈ V
92 simpl 484 . . . . . . . . . 10 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ π‘₯ = 𝑒)
9392eleq1d 2823 . . . . . . . . 9 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ (π‘₯ ∈ 𝐴 ↔ 𝑒 ∈ 𝐴))
94 simpr 486 . . . . . . . . . 10 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ 𝑦 = 𝑣)
9592fveq2d 6851 . . . . . . . . . 10 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ (π‘“β€˜π‘₯) = (π‘“β€˜π‘’))
9694, 95eleq12d 2832 . . . . . . . . 9 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ (𝑦 ∈ (π‘“β€˜π‘₯) ↔ 𝑣 ∈ (π‘“β€˜π‘’)))
9793, 96anbi12d 632 . . . . . . . 8 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ ((π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯)) ↔ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’))))
9863, 91, 97opelopaba 5498 . . . . . . 7 (βŸ¨π‘’, π‘£βŸ© ∈ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))} ↔ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’)))
99 breq2 5114 . . . . . . . . . . . 12 (𝑏 = 𝑣 β†’ (π‘’π‘Ÿπ‘ ↔ π‘’π‘Ÿπ‘£))
100 df-br 5111 . . . . . . . . . . . 12 (π‘’π‘Ÿπ‘£ ↔ βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ)
10199, 100bitrdi 287 . . . . . . . . . . 11 (𝑏 = 𝑣 β†’ (π‘’π‘Ÿπ‘ ↔ βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ))
102101elrab 3650 . . . . . . . . . 10 (𝑣 ∈ {𝑏 ∈ 𝐡 ∣ π‘’π‘Ÿπ‘} ↔ (𝑣 ∈ 𝐡 ∧ βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ))
103102anbi2i 624 . . . . . . . . 9 ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ {𝑏 ∈ 𝐡 ∣ π‘’π‘Ÿπ‘}) ↔ (𝑒 ∈ 𝐴 ∧ (𝑣 ∈ 𝐡 ∧ βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ)))
104103a1i 11 . . . . . . . 8 (((𝐡 ∈ π‘Š ∧ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡)) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) β†’ ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ {𝑏 ∈ 𝐡 ∣ π‘’π‘Ÿπ‘}) ↔ (𝑒 ∈ 𝐴 ∧ (𝑣 ∈ 𝐡 ∧ βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ))))
105 simplr 768 . . . . . . . . . . . 12 ((((𝐡 ∈ π‘Š ∧ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡)) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) ∧ 𝑒 ∈ 𝐴) β†’ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦}))
106 breq1 5113 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Ž β†’ (π‘₯π‘Ÿπ‘¦ ↔ π‘Žπ‘Ÿπ‘¦))
107106rabbidv 3418 . . . . . . . . . . . . . 14 (π‘₯ = π‘Ž β†’ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦} = {𝑦 ∈ 𝐡 ∣ π‘Žπ‘Ÿπ‘¦})
108 breq2 5114 . . . . . . . . . . . . . . 15 (𝑦 = 𝑏 β†’ (π‘Žπ‘Ÿπ‘¦ ↔ π‘Žπ‘Ÿπ‘))
109108cbvrabv 3420 . . . . . . . . . . . . . 14 {𝑦 ∈ 𝐡 ∣ π‘Žπ‘Ÿπ‘¦} = {𝑏 ∈ 𝐡 ∣ π‘Žπ‘Ÿπ‘}
110107, 109eqtrdi 2793 . . . . . . . . . . . . 13 (π‘₯ = π‘Ž β†’ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦} = {𝑏 ∈ 𝐡 ∣ π‘Žπ‘Ÿπ‘})
111110cbvmptv 5223 . . . . . . . . . . . 12 (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦}) = (π‘Ž ∈ 𝐴 ↦ {𝑏 ∈ 𝐡 ∣ π‘Žπ‘Ÿπ‘})
112105, 111eqtrdi 2793 . . . . . . . . . . 11 ((((𝐡 ∈ π‘Š ∧ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡)) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) ∧ 𝑒 ∈ 𝐴) β†’ 𝑓 = (π‘Ž ∈ 𝐴 ↦ {𝑏 ∈ 𝐡 ∣ π‘Žπ‘Ÿπ‘}))
113 breq1 5113 . . . . . . . . . . . . 13 (π‘Ž = 𝑒 β†’ (π‘Žπ‘Ÿπ‘ ↔ π‘’π‘Ÿπ‘))
114113rabbidv 3418 . . . . . . . . . . . 12 (π‘Ž = 𝑒 β†’ {𝑏 ∈ 𝐡 ∣ π‘Žπ‘Ÿπ‘} = {𝑏 ∈ 𝐡 ∣ π‘’π‘Ÿπ‘})
115114adantl 483 . . . . . . . . . . 11 (((((𝐡 ∈ π‘Š ∧ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡)) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) ∧ 𝑒 ∈ 𝐴) ∧ π‘Ž = 𝑒) β†’ {𝑏 ∈ 𝐡 ∣ π‘Žπ‘Ÿπ‘} = {𝑏 ∈ 𝐡 ∣ π‘’π‘Ÿπ‘})
116 simpr 486 . . . . . . . . . . 11 ((((𝐡 ∈ π‘Š ∧ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡)) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) ∧ 𝑒 ∈ 𝐴) β†’ 𝑒 ∈ 𝐴)
117 rabexg 5293 . . . . . . . . . . . 12 (𝐡 ∈ π‘Š β†’ {𝑏 ∈ 𝐡 ∣ π‘’π‘Ÿπ‘} ∈ V)
118117ad3antrrr 729 . . . . . . . . . . 11 ((((𝐡 ∈ π‘Š ∧ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡)) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) ∧ 𝑒 ∈ 𝐴) β†’ {𝑏 ∈ 𝐡 ∣ π‘’π‘Ÿπ‘} ∈ V)
119112, 115, 116, 118fvmptd 6960 . . . . . . . . . 10 ((((𝐡 ∈ π‘Š ∧ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡)) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) ∧ 𝑒 ∈ 𝐴) β†’ (π‘“β€˜π‘’) = {𝑏 ∈ 𝐡 ∣ π‘’π‘Ÿπ‘})
120119eleq2d 2824 . . . . . . . . 9 ((((𝐡 ∈ π‘Š ∧ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡)) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) ∧ 𝑒 ∈ 𝐴) β†’ (𝑣 ∈ (π‘“β€˜π‘’) ↔ 𝑣 ∈ {𝑏 ∈ 𝐡 ∣ π‘’π‘Ÿπ‘}))
121120pm5.32da 580 . . . . . . . 8 (((𝐡 ∈ π‘Š ∧ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡)) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) β†’ ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’)) ↔ (𝑒 ∈ 𝐴 ∧ 𝑣 ∈ {𝑏 ∈ 𝐡 ∣ π‘’π‘Ÿπ‘})))
122 simplr 768 . . . . . . . . . 10 (((𝐡 ∈ π‘Š ∧ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡)) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) β†’ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡))
123122elpwid 4574 . . . . . . . . 9 (((𝐡 ∈ π‘Š ∧ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡)) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) β†’ π‘Ÿ βŠ† (𝐴 Γ— 𝐡))
12463, 91opeldm 5868 . . . . . . . . . . . 12 (βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ β†’ 𝑒 ∈ dom π‘Ÿ)
125 dmss 5863 . . . . . . . . . . . . . 14 (π‘Ÿ βŠ† (𝐴 Γ— 𝐡) β†’ dom π‘Ÿ βŠ† dom (𝐴 Γ— 𝐡))
126 dmxpss 6128 . . . . . . . . . . . . . 14 dom (𝐴 Γ— 𝐡) βŠ† 𝐴
127125, 126sstrdi 3961 . . . . . . . . . . . . 13 (π‘Ÿ βŠ† (𝐴 Γ— 𝐡) β†’ dom π‘Ÿ βŠ† 𝐴)
128127sseld 3948 . . . . . . . . . . . 12 (π‘Ÿ βŠ† (𝐴 Γ— 𝐡) β†’ (𝑒 ∈ dom π‘Ÿ β†’ 𝑒 ∈ 𝐴))
129124, 128syl5 34 . . . . . . . . . . 11 (π‘Ÿ βŠ† (𝐴 Γ— 𝐡) β†’ (βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ β†’ 𝑒 ∈ 𝐴))
130129pm4.71rd 564 . . . . . . . . . 10 (π‘Ÿ βŠ† (𝐴 Γ— 𝐡) β†’ (βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ ↔ (𝑒 ∈ 𝐴 ∧ βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ)))
13163, 91opelrn 5903 . . . . . . . . . . . . 13 (βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ β†’ 𝑣 ∈ ran π‘Ÿ)
132 rnss 5899 . . . . . . . . . . . . . . 15 (π‘Ÿ βŠ† (𝐴 Γ— 𝐡) β†’ ran π‘Ÿ βŠ† ran (𝐴 Γ— 𝐡))
133 rnxpss 6129 . . . . . . . . . . . . . . 15 ran (𝐴 Γ— 𝐡) βŠ† 𝐡
134132, 133sstrdi 3961 . . . . . . . . . . . . . 14 (π‘Ÿ βŠ† (𝐴 Γ— 𝐡) β†’ ran π‘Ÿ βŠ† 𝐡)
135134sseld 3948 . . . . . . . . . . . . 13 (π‘Ÿ βŠ† (𝐴 Γ— 𝐡) β†’ (𝑣 ∈ ran π‘Ÿ β†’ 𝑣 ∈ 𝐡))
136131, 135syl5 34 . . . . . . . . . . . 12 (π‘Ÿ βŠ† (𝐴 Γ— 𝐡) β†’ (βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ β†’ 𝑣 ∈ 𝐡))
137136pm4.71rd 564 . . . . . . . . . . 11 (π‘Ÿ βŠ† (𝐴 Γ— 𝐡) β†’ (βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ ↔ (𝑣 ∈ 𝐡 ∧ βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ)))
138137anbi2d 630 . . . . . . . . . 10 (π‘Ÿ βŠ† (𝐴 Γ— 𝐡) β†’ ((𝑒 ∈ 𝐴 ∧ βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ) ↔ (𝑒 ∈ 𝐴 ∧ (𝑣 ∈ 𝐡 ∧ βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ))))
139130, 138bitrd 279 . . . . . . . . 9 (π‘Ÿ βŠ† (𝐴 Γ— 𝐡) β†’ (βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ ↔ (𝑒 ∈ 𝐴 ∧ (𝑣 ∈ 𝐡 ∧ βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ))))
140123, 139syl 17 . . . . . . . 8 (((𝐡 ∈ π‘Š ∧ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡)) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) β†’ (βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ ↔ (𝑒 ∈ 𝐴 ∧ (𝑣 ∈ 𝐡 ∧ βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ))))
141104, 121, 1403bitr4d 311 . . . . . . 7 (((𝐡 ∈ π‘Š ∧ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡)) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) β†’ ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ (π‘“β€˜π‘’)) ↔ βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ))
14298, 141bitr2id 284 . . . . . 6 (((𝐡 ∈ π‘Š ∧ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡)) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) β†’ (βŸ¨π‘’, π‘£βŸ© ∈ π‘Ÿ ↔ βŸ¨π‘’, π‘£βŸ© ∈ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}))
143142eqrelrdv2 5756 . . . . 5 (((Rel π‘Ÿ ∧ Rel {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ∧ ((𝐡 ∈ π‘Š ∧ π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡)) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦}))) β†’ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))})
14485, 87, 90, 143syl21anc 837 . . . 4 (((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) ∧ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) β†’ π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))})
14579, 144impbida 800 . . 3 ((πœ‘ ∧ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝐴))) β†’ (π‘Ÿ = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))} ↔ 𝑓 = (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})))
1461, 12, 28, 145f1ocnv2d 7611 . 2 (πœ‘ β†’ ((π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})):𝒫 (𝐴 Γ— 𝐡)–1-1-ontoβ†’(𝒫 𝐡 ↑m 𝐴) ∧ β—‘(π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) = (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))})))
147 rfovcnvf1od.f . . . 4 𝐹 = (𝐴𝑂𝐡)
148 rfovd.rf . . . . 5 𝑂 = (π‘Ž ∈ V, 𝑏 ∈ V ↦ (π‘Ÿ ∈ 𝒫 (π‘Ž Γ— 𝑏) ↦ (π‘₯ ∈ π‘Ž ↦ {𝑦 ∈ 𝑏 ∣ π‘₯π‘Ÿπ‘¦})))
149148, 9, 2rfovd 42347 . . . 4 (πœ‘ β†’ (𝐴𝑂𝐡) = (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})))
150147, 149eqtrid 2789 . . 3 (πœ‘ β†’ 𝐹 = (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})))
151 f1oeq1 6777 . . . 4 (𝐹 = (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) β†’ (𝐹:𝒫 (𝐴 Γ— 𝐡)–1-1-ontoβ†’(𝒫 𝐡 ↑m 𝐴) ↔ (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})):𝒫 (𝐴 Γ— 𝐡)–1-1-ontoβ†’(𝒫 𝐡 ↑m 𝐴)))
152 cnveq 5834 . . . . 5 (𝐹 = (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) β†’ ◑𝐹 = β—‘(π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})))
153152eqeq1d 2739 . . . 4 (𝐹 = (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) β†’ (◑𝐹 = (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}) ↔ β—‘(π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) = (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))})))
154151, 153anbi12d 632 . . 3 (𝐹 = (π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) β†’ ((𝐹:𝒫 (𝐴 Γ— 𝐡)–1-1-ontoβ†’(𝒫 𝐡 ↑m 𝐴) ∧ ◑𝐹 = (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))})) ↔ ((π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})):𝒫 (𝐴 Γ— 𝐡)–1-1-ontoβ†’(𝒫 𝐡 ↑m 𝐴) ∧ β—‘(π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) = (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}))))
155150, 154syl 17 . 2 (πœ‘ β†’ ((𝐹:𝒫 (𝐴 Γ— 𝐡)–1-1-ontoβ†’(𝒫 𝐡 ↑m 𝐴) ∧ ◑𝐹 = (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))})) ↔ ((π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})):𝒫 (𝐴 Γ— 𝐡)–1-1-ontoβ†’(𝒫 𝐡 ↑m 𝐴) ∧ β—‘(π‘Ÿ ∈ 𝒫 (𝐴 Γ— 𝐡) ↦ (π‘₯ ∈ 𝐴 ↦ {𝑦 ∈ 𝐡 ∣ π‘₯π‘Ÿπ‘¦})) = (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))}))))
156146, 155mpbird 257 1 (πœ‘ β†’ (𝐹:𝒫 (𝐴 Γ— 𝐡)–1-1-ontoβ†’(𝒫 𝐡 ↑m 𝐴) ∧ ◑𝐹 = (𝑓 ∈ (𝒫 𝐡 ↑m 𝐴) ↦ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ (π‘“β€˜π‘₯))})))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542  βŠ€wtru 1543   ∈ wcel 2107  βˆ€wral 3065  {crab 3410  Vcvv 3448   ∩ cin 3914   βŠ† wss 3915  π’« cpw 4565  βŸ¨cop 4597   class class class wbr 5110  {copab 5172   ↦ cmpt 5193   Γ— cxp 5636  β—‘ccnv 5637  dom cdm 5638  ran crn 5639  Rel wrel 5643   Fn wfn 6496  βŸΆwf 6497  β€“1-1-ontoβ†’wf1o 6500  β€˜cfv 6501  (class class class)co 7362   ∈ cmpo 7364   ↑m cmap 8772
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-1st 7926  df-2nd 7927  df-map 8774
This theorem is referenced by:  rfovcnvd  42351  rfovf1od  42352
  Copyright terms: Public domain W3C validator