Theorem fliftcnv 5356

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 2018	. . . . 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 5353	. . . 4 ⊢ (φ → ran (x ∈ 𝑋 ↦ ⟨B, A⟩) ⊆ (𝑆 × 𝑅))
5		relxp 4370	. . . 4 ⊢ Rel (𝑆 × 𝑅)
6		relss 4350	. . . 4 ⊢ (ran (x ∈ 𝑋 ↦ ⟨B, A⟩) ⊆ (𝑆 × 𝑅) → (Rel (𝑆 × 𝑅) → Rel ran (x ∈ 𝑋 ↦ ⟨B, A⟩)))
7	4, 5, 6	mpisyl 1311	. . 3 ⊢ (φ → Rel ran (x ∈ 𝑋 ↦ ⟨B, A⟩))
8		relcnv 4626	. . 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 5354	. . . . . 6 ⊢ (φ → (z𝐹y ↔ ∃x ∈ 𝑋 (z = A ∧ y = B)))
12		vex 2534	. . . . . . 7 ⊢ y ∈ V
13		vex 2534	. . . . . . 7 ⊢ z ∈ V
14	12, 13	brcnv 4441	. . . . . 6 ⊢ (y◡𝐹z ↔ z𝐹y)
15		ancom 253	. . . . . . 7 ⊢ ((y = B ∧ z = A) ↔ (z = A ∧ y = B))
16	15	rexbii 2305	. . . . . 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 5354	. . . . 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 3735	. . . 4 ⊢ (y◡𝐹z ↔ ⟨y, z⟩ ∈ ◡𝐹)
21		df-br 3735	. . . 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 4362	. 2 ⊢ (((Rel ◡𝐹 ∧ Rel ran (x ∈ 𝑋 ↦ ⟨B, A⟩)) ∧ φ) → ◡𝐹 = ran (x ∈ 𝑋 ↦ ⟨B, A⟩))
24	9, 23	mpancom 401	1 ⊢ (φ → ◡𝐹 = ran (x ∈ 𝑋 ↦ ⟨B, A⟩))

Syntax hints:   → wi 4   ∧ wa 97   = wceq 1226   ∈ wcel 1370  ∃wrex 2281   ⊆ wss 2890  ⟨cop 3349   class class class wbr 3734   ↦ cmpt 3788   × cxp 4266  ^◡ccnv 4267  ran crn 4269  Rel wrel 4273

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 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-rab 2289  df-v 2533  df-sbc 2738  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-br 3735  df-opab 3789  df-mpt 3790  df-id 4000  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-dm 4278  df-rn 4279  df-res 4280  df-ima 4281  df-iota 4790  df-fun 4827  df-fn 4828  df-f 4829  df-fv 4833

This theorem is referenced by: (None)