Metamath Proof Explorer

Theorem ismrcd2

Description: Second half of ismrcd1 . (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypotheses ismrcd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
ismrcd.f ⊢ ( 𝜑 → 𝐹 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
ismrcd.e ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) )
ismrcd.m ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
ismrcd.i ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
Assertion ismrcd2 ( 𝜑 → 𝐹 = ( mrCls ‘ dom ( 𝐹 ∩ I ) ) )

Proof

Step Hyp Ref Expression
1 ismrcd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
2 ismrcd.f ⊢ ( 𝜑 → 𝐹 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
3 ismrcd.e ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) )
4 ismrcd.m ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
5 ismrcd.i ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
6 2 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝒫 𝐵 )
7 1 2 3 4 5 ismrcd1 ⊢ ( 𝜑 → dom ( 𝐹 ∩ I ) ∈ ( Moore ‘ 𝐵 ) )
8 eqid ⊢ ( mrCls ‘ dom ( 𝐹 ∩ I ) ) = ( mrCls ‘ dom ( 𝐹 ∩ I ) )
9 8 mrcf ⊢ ( dom ( 𝐹 ∩ I ) ∈ ( Moore ‘ 𝐵 ) → ( mrCls ‘ dom ( 𝐹 ∩ I ) ) : 𝒫 𝐵 ⟶ dom ( 𝐹 ∩ I ) )
10 ffn ⊢ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) : 𝒫 𝐵 ⟶ dom ( 𝐹 ∩ I ) → ( mrCls ‘ dom ( 𝐹 ∩ I ) ) Fn 𝒫 𝐵 )
11 7 9 10 3syl ⊢ ( 𝜑 → ( mrCls ‘ dom ( 𝐹 ∩ I ) ) Fn 𝒫 𝐵 )
12 7 8 mrcssvd ⊢ ( 𝜑 → ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ⊆ 𝐵 )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ⊆ 𝐵 )
14 elpwi ⊢ ( 𝑧 ∈ 𝒫 𝐵 → 𝑧 ⊆ 𝐵 )
15 8 mrcssid ⊢ ( ( dom ( 𝐹 ∩ I ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝑧 ⊆ 𝐵 ) → 𝑧 ⊆ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) )
16 7 14 15 syl2an ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → 𝑧 ⊆ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) )
17 4 3expib ⊢ ( 𝜑 → ( ( 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) )
18 17 alrimivv ⊢ ( 𝜑 → ∀ 𝑦 ∀ 𝑥 ( ( 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) )
19 vex ⊢ 𝑧 ∈ V
20 fvex ⊢ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ∈ V
21 sseq1 ⊢ ( 𝑥 = ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) → ( 𝑥 ⊆ 𝐵 ↔ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ⊆ 𝐵 ) )
22 21 adantl ⊢ ( ( 𝑦 = 𝑧 ∧ 𝑥 = ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) → ( 𝑥 ⊆ 𝐵 ↔ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ⊆ 𝐵 ) )
23 sseq12 ⊢ ( ( 𝑦 = 𝑧 ∧ 𝑥 = ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) → ( 𝑦 ⊆ 𝑥 ↔ 𝑧 ⊆ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) )
24 22 23 anbi12d ⊢ ( ( 𝑦 = 𝑧 ∧ 𝑥 = ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) → ( ( 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) ↔ ( ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ⊆ 𝐵 ∧ 𝑧 ⊆ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) ) )
25 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) )
26 fveq2 ⊢ ( 𝑥 = ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) )
27 sseq12 ⊢ ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) ) → ( ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑧 ) ⊆ ( 𝐹 ‘ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) ) )
28 25 26 27 syl2an ⊢ ( ( 𝑦 = 𝑧 ∧ 𝑥 = ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) → ( ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑧 ) ⊆ ( 𝐹 ‘ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) ) )
29 24 28 imbi12d ⊢ ( ( 𝑦 = 𝑧 ∧ 𝑥 = ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) → ( ( ( 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ⊆ 𝐵 ∧ 𝑧 ⊆ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) → ( 𝐹 ‘ 𝑧 ) ⊆ ( 𝐹 ‘ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) ) ) )
30 29 spc2gv ⊢ ( ( 𝑧 ∈ V ∧ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ∈ V ) → ( ∀ 𝑦 ∀ 𝑥 ( ( 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ( ( ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ⊆ 𝐵 ∧ 𝑧 ⊆ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) → ( 𝐹 ‘ 𝑧 ) ⊆ ( 𝐹 ‘ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) ) ) )
31 19 20 30 mp2an ⊢ ( ∀ 𝑦 ∀ 𝑥 ( ( 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ( ( ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ⊆ 𝐵 ∧ 𝑧 ⊆ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) → ( 𝐹 ‘ 𝑧 ) ⊆ ( 𝐹 ‘ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) ) )
32 18 31 syl ⊢ ( 𝜑 → ( ( ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ⊆ 𝐵 ∧ 𝑧 ⊆ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) → ( 𝐹 ‘ 𝑧 ) ⊆ ( 𝐹 ‘ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → ( ( ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ⊆ 𝐵 ∧ 𝑧 ⊆ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) → ( 𝐹 ‘ 𝑧 ) ⊆ ( 𝐹 ‘ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) ) )
34 13 16 33 mp2and ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → ( 𝐹 ‘ 𝑧 ) ⊆ ( 𝐹 ‘ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) )
35 8 mrccl ⊢ ( ( dom ( 𝐹 ∩ I ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝑧 ⊆ 𝐵 ) → ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) )
36 7 14 35 syl2an ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) )
37 6 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → 𝐹 Fn 𝒫 𝐵 )
38 20 elpw ⊢ ( ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ∈ 𝒫 𝐵 ↔ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ⊆ 𝐵 )
39 12 38 sylibr ⊢ ( 𝜑 → ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ∈ 𝒫 𝐵 )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ∈ 𝒫 𝐵 )
41 fnelfp ⊢ ( ( 𝐹 Fn 𝒫 𝐵 ∧ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ∈ 𝒫 𝐵 ) → ( ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) = ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) )
42 37 40 41 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → ( ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) = ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) )
43 36 42 mpbid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → ( 𝐹 ‘ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ) = ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) )
44 34 43 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → ( 𝐹 ‘ 𝑧 ) ⊆ ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) )
45 7 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → dom ( 𝐹 ∩ I ) ∈ ( Moore ‘ 𝐵 ) )
46 sseq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ⊆ 𝐵 ↔ 𝑧 ⊆ 𝐵 ) )
47 46 anbi2d ⊢ ( 𝑥 = 𝑧 → ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ) )
48 id ⊢ ( 𝑥 = 𝑧 → 𝑥 = 𝑧 )
49 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
50 48 49 sseq12d ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) ↔ 𝑧 ⊆ ( 𝐹 ‘ 𝑧 ) ) )
51 47 50 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) → 𝑧 ⊆ ( 𝐹 ‘ 𝑧 ) ) ) )
52 51 3 chvarvv ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) → 𝑧 ⊆ ( 𝐹 ‘ 𝑧 ) )
53 14 52 sylan2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → 𝑧 ⊆ ( 𝐹 ‘ 𝑧 ) )
54 2fveq3 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝐹 ‘ 𝑧 ) ) )
55 54 49 eqeq12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ 𝑧 ) ) )
56 47 55 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ 𝑧 ) ) ) )
57 56 5 chvarvv ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ 𝑧 ) )
58 14 57 sylan2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ 𝑧 ) )
59 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝒫 𝐵 )
60 fnelfp ⊢ ( ( 𝐹 Fn 𝒫 𝐵 ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝒫 𝐵 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ 𝑧 ) ) )
61 37 59 60 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ 𝑧 ) ) )
62 58 61 mpbird ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → ( 𝐹 ‘ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) )
63 8 mrcsscl ⊢ ( ( dom ( 𝐹 ∩ I ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝑧 ⊆ ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ dom ( 𝐹 ∩ I ) ) → ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ⊆ ( 𝐹 ‘ 𝑧 ) )
64 45 53 62 63 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) ⊆ ( 𝐹 ‘ 𝑧 ) )
65 44 64 eqssd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝐵 ) → ( 𝐹 ‘ 𝑧 ) = ( ( mrCls ‘ dom ( 𝐹 ∩ I ) ) ‘ 𝑧 ) )
66 6 11 65 eqfnfvd ⊢ ( 𝜑 → 𝐹 = ( mrCls ‘ dom ( 𝐹 ∩ I ) ) )