Theorem fliftcnv 5378

Description: Converse of the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)

Hypotheses

Ref	Expression
flift.1	⊢ 𝐹 = ran (x ∈ 𝑋 ↦ ⟨A, B⟩)
flift.2	⊢ ((φ ∧ x ∈ 𝑋) → A ∈ 𝑅)
flift.3	⊢ ((φ ∧ x ∈ 𝑋) → B ∈ 𝑆)

Assertion

Ref	Expression
fliftcnv	⊢ (φ → ◡𝐹 = ran (x ∈ 𝑋 ↦ ⟨B, A⟩))

Distinct variable groups:   x,𝑅   φ,x   x,𝑋   x,𝑆

Allowed substitution hints:   A(x)   B(x)   𝐹(x)

Proof of Theorem fliftcnv

Dummy variables y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2037	. . . . 5 ⊢ ran (x ∈ 𝑋 ↦ ⟨B, A⟩) = ran (x ∈ 𝑋 ↦ ⟨B, A⟩)
2		flift.3	. . . . 5 ⊢ ((φ ∧ x ∈ 𝑋) → B ∈ 𝑆)
3		flift.2	. . . . 5 ⊢ ((φ ∧ x ∈ 𝑋) → A ∈ 𝑅)
4	1, 2, 3	fliftrel 5375	. . . 4 ⊢ (φ → ran (x ∈ 𝑋 ↦ ⟨B, A⟩) ⊆ (𝑆 × 𝑅))
5		relxp 4390	. . . 4 ⊢ Rel (𝑆 × 𝑅)
6		relss 4370	. . . 4 ⊢ (ran (x ∈ 𝑋 ↦ ⟨B, A⟩) ⊆ (𝑆 × 𝑅) → (Rel (𝑆 × 𝑅) → Rel ran (x ∈ 𝑋 ↦ ⟨B, A⟩)))
7	4, 5, 6	mpisyl 1332	. . 3 ⊢ (φ → Rel ran (x ∈ 𝑋 ↦ ⟨B, A⟩))
8		relcnv 4646	. . 3 ⊢ Rel ◡𝐹
9	7, 8	jctil 295	. 2 ⊢ (φ → (Rel ◡𝐹 ∧ Rel ran (x ∈ 𝑋 ↦ ⟨B, A⟩)))
10		flift.1	. . . . . . 7 ⊢ 𝐹 = ran (x ∈ 𝑋 ↦ ⟨A, B⟩)
11	10, 3, 2	fliftel 5376	. . . . . 6 ⊢ (φ → (z𝐹y ↔ ∃x ∈ 𝑋 (z = A ∧ y = B)))
12		vex 2554	. . . . . . 7 ⊢ y ∈ V
13		vex 2554	. . . . . . 7 ⊢ z ∈ V
14	12, 13	brcnv 4461	. . . . . 6 ⊢ (y◡𝐹z ↔ z𝐹y)
15		ancom 253	. . . . . . 7 ⊢ ((y = B ∧ z = A) ↔ (z = A ∧ y = B))
16	15	rexbii 2325	. . . . . 6 ⊢ (∃x ∈ 𝑋 (y = B ∧ z = A) ↔ ∃x ∈ 𝑋 (z = A ∧ y = B))
17	11, 14, 16	3bitr4g 212	. . . . 5 ⊢ (φ → (y◡𝐹z ↔ ∃x ∈ 𝑋 (y = B ∧ z = A)))
18	1, 2, 3	fliftel 5376	. . . . 5 ⊢ (φ → (yran (x ∈ 𝑋 ↦ ⟨B, A⟩)z ↔ ∃x ∈ 𝑋 (y = B ∧ z = A)))
19	17, 18	bitr4d 180	. . . 4 ⊢ (φ → (y◡𝐹z ↔ yran (x ∈ 𝑋 ↦ ⟨B, A⟩)z))
20		df-br 3756	. . . 4 ⊢ (y◡𝐹z ↔ ⟨y, z⟩ ∈ ◡𝐹)
21		df-br 3756	. . . 4 ⊢ (yran (x ∈ 𝑋 ↦ ⟨B, A⟩)z ↔ ⟨y, z⟩ ∈ ran (x ∈ 𝑋 ↦ ⟨B, A⟩))
22	19, 20, 21	3bitr3g 211	. . 3 ⊢ (φ → (⟨y, z⟩ ∈ ◡𝐹 ↔ ⟨y, z⟩ ∈ ran (x ∈ 𝑋 ↦ ⟨B, A⟩)))
23	22	eqrelrdv2 4382	. 2 ⊢ (((Rel ◡𝐹 ∧ Rel ran (x ∈ 𝑋 ↦ ⟨B, A⟩)) ∧ φ) → ◡𝐹 = ran (x ∈ 𝑋 ↦ ⟨B, A⟩))
24	9, 23	mpancom 399	1 ⊢ (φ → ◡𝐹 = ran (x ∈ 𝑋 ↦ ⟨B, A⟩))

Syntax hints:   → wi 4   ∧ wa 97   = wceq 1242   ∈ wcel 1390  ∃wrex 2301   ⊆ wss 2911  ⟨cop 3370   class class class wbr 3755   ↦ cmpt 3809   × cxp 4286  ^◡ccnv 4287  ran crn 4289  Rel wrel 4293

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-fv 4853

This theorem is referenced by: (None)